Accéder directement au contenu Accéder directement à la navigation
Communication dans un congrès

KriQL: a query language for the diagnosis of transition systems

Khaoula Es-Salhi 1, 2 Siham Rim Boudaoud 1 Ciprian Teodorov 1, 3 Zoé Drey 1, 3 Vincent Ribaud 4
1 Lab-STICC_ENSTAB_CACS_MOCS ; IDM
STIC - Pôle STIC [Brest], Lab-STICC - Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance
3 Lab-STICC_ENSTAB_CACS_MOCS
Lab-STICC - Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance (UMR 3192)
4 Lab-STICC_UBO_CACS_MOCS
Lab-STICC - Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance, UBO - Université de Brest
Abstract : The formal verification of a concurrent system with a model-checker provides the user with a counterexample trace when a property is violated; however the problem diagnosis still remain a complex issue. Diagnosis is made difficult for several reasons: the trace conforms to a structure that is internal to the verification tool and hence hard to exploit, the trace yields low-level information, the trace size can be large. Traces cannot be understood without the Labelled Transition System (LTS) underlying the model-checker exhaustive exploration; we designed KriQL a query language over the LTS graph featuring a blend of set filters and graph-based operations and we implemented some feasibility prototypes. Benchmark results indicate that a hybrid management system using a graph-based database and dedicated data structures should achieve sufficient performances.
Liste complète des métadonnées

Littérature citée [17 références]  Voir  Masquer  Télécharger

https://hal.archives-ouvertes.fr/hal-01203649
Contributeur : Annick Billon-Coat <>
Soumis le : lundi 13 février 2017 - 13:20:42
Dernière modification le : vendredi 7 août 2020 - 15:56:05
Archivage à long terme le : : dimanche 14 mai 2017 - 13:52:09

Fichier

KriQL_ a query language for la...
Fichiers éditeurs autorisés sur une archive ouverte

Identifiants

  • HAL Id : hal-01203649, version 1

Citation

Khaoula Es-Salhi, Siham Rim Boudaoud, Ciprian Teodorov, Zoé Drey, Vincent Ribaud. KriQL: a query language for the diagnosis of transition systems. 15th International Workshop on Automated Verification of Critical Systems - AVOCS'15, Sep 2015, Edimburgh, United Kingdom. pp.151-165. ⟨hal-01203649⟩

Partager

Métriques

Consultations de la notice

619

Téléchargements de fichiers

93