 |
Communication dans un congrès
KriQL: a query language for the diagnosis of transition systems
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.
Littérature citée [17 références]
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
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