Relational and graph queries over a transition system - Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance, site de l'UBO Accéder directement au contenu
Communication Dans Un Congrès Année : 2015

Relational and graph queries over a transition system

Résumé

Explicit model-checking is a brute force traversal of all possible model states that permits to assert if a property is satisfied or not. If the property is violated, the model-checker produces a counterexample trace. However, once the existence of a problem is proved, the designer is left with a counterexample trace that only exhibits the problem. The designer needs to interpret traces and this interpretation is challenging for several reasons such as the trace size or the low-level of information. We believe that querying traces will help the problem interpretation because it supports visualization and diagnosis tools. We designed KriQL, a query language working on traces and the underlying labelled transition system. This paper evaluates different KriQl implementations, mainly the use of relational and graph databases for the management of the transition system. We present results obtained through the analysis of a Cruise-Control System, a realistic case study from the automotive industry.
Fichier principal
Vignette du fichier
RelationalAndGraphQueriesOverATransitionSystem.pdf (1006.23 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01203662 , version 1 (13-02-2017)

Identifiants

Citer

Siham Rim Boudaoud, Khaoula Es-Salhi, Vincent Ribaud, Ciprian Teodorov. Relational and graph queries over a transition system. International Conference on Computer as a Tool (EUROCON 2015), Sep 2015, Salamanque, Spain. pp.1-6, ⟨10.1109/EUROCON.2015.7313738⟩. ⟨hal-01203662⟩
238 Consultations
207 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More