%0 Conference Paper
%F Oral 
%T KriQL: a query language for the diagnosis of transition systems
%+ Lab-STICC_ENSTAB_CACS_MOCS
%+ Université de Brest (UBO)
%+ Lab-STICC_UBO_CACS_MOCS
%A Es-Salhi, Khaoula
%A Boudaoud, Siham Rim
%A Teodorov, Ciprian
%A Drey, Zoé
%A Ribaud, Vincent
%< avec comité de lecture
%B 15th International Workshop on Automated Verification of Critical Systems - AVOCS'15
%C Edimburgh, United Kingdom
%S Pre-proceedings of the 15th International Workshop on Automated Verification of Critical Systems
%P 151-165
%8 2015-09-01
%D 2015
%K trace
%K transition system
%K query language
%Z Computer Science [cs]/Software Engineering [cs.SE]
%Z Computer Science [cs]/Formal Languages and Automata Theory [cs.FL]
%Z Computer Science [cs]/Modeling and SimulationConference papers
%X 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.
%G English
%2 https://hal.science/hal-01203649/document
%2 https://hal.science/hal-01203649/file/KriQL_%20a%20query%20language%20for%20labelled%20transition%20systems.pdf
%L hal-01203649
%U https://hal.science/hal-01203649
%~ UNIV-BREST
%~ INSTITUT-TELECOM
%~ ENSTA-BRETAGNE
%~ CNRS
%~ UNIV-UBS
%~ ENSTA-BRETAGNE-STIC
%~ LAB-STICC_UBO_CACS
%~ LAB-STICC_UBO
%~ ENIB
%~ LAB-STICC_ENIB
%~ LAB-STICC
%~ TDS-MACS
%~ IBNM
%~ INSTITUTS-TELECOM