KriQL: a query language for the diagnosis of transition systems

Khaoula Es-Salhi (1, 2) , Siham Rim Boudaoud (1) , Ciprian Teodorov (1, 1) , Zoé Drey (1, 1) , Vincent Ribaud (3)

1 Lab-STICC_ENSTAB_CACS_MOCS
2 UBO - Université de Brest
3 Lab-STICC_UBO_CACS_MOCS

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.

Mots clés: trace; transition system; query language

Domaines: Génie logiciel [cs.SE]; Théorie et langage formel [cs.FL]; Modélisation et simulation

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⟩