Debugging of Concurrent Systems using Counterexample Analysis

Gianluca Barbon 1 Vincent Leroy 2 Gwen Salaün 1
1 CONVECS - Construction of verified concurrent systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
2 SLIDE - ScaLable Information Discovery and Exploitation [Saint Martin d’Hères]
LIG - Laboratoire d'Informatique de Grenoble
Abstract : Model checking is an established technique for automatically verifying that a model satisfies a given temporal property. When the model violates the property, the model checker returns a counterexample , which is a sequence of actions leading to a state where the property is not satisfied. Understanding this counterexample for debugging the specification is a complicated task for several reasons: (i) the counterexample can contain hundreds of actions, (ii) the debugging task is mostly achieved manually, and (iii) the counterexample does not give any clue on the state of the system (e.g., parallelism or data expressions) when the error occurs. This paper presents a new approach that improves the usability of model checking by simplifying the comprehension of counterexamples. Our solution aims at keeping only actions in counterexamples that are relevant for debugging purposes. To do so, we first extract in the model all the counterexamples. Second, we define an analysis algorithm that identifies actions that make the behaviour skip from incorrect to correct behaviours, making these actions relevant from a debugging perspective. Our approach is fully automated by a tool that we implemented and applied on real-world case studies from various application areas for evaluation purposes.
Keywords : Model Checking Debugging Counterexamples Concurrent Systems
Type de document :
Communication dans un congrès
Mehdi Dastani; Marjan Sirjani. 7th International Conference on Fundamentals of Software Engineering (FSEN), Apr 2017, Tehran, Iran. Springer Verlag, Lecture Notes in Computer Science, LNCS-10522, pp.20-34, 2017, Fundamentals of Software Engineering. 〈http://fsen.ir/2017/〉. 〈10.1007/978-3-319-68972-2_2〉
Liste complète des métadonnées

Littérature citée [24 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/hal-01533401
Contributeur : Gianluca Barbon <>
Soumis le : vendredi 4 août 2017 - 16:57:45
Dernière modification le : mercredi 11 avril 2018 - 01:55:23

Fichier

fsen17_rev.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

LIG_SRCPR | CONVECS | LIG | LIG-TDCGE-SLIDE | INRIA2017 | INRIA | UGA | INRIA-RENGRE | IFIP-TC | IFIP-TC2 | IFIP | IFIP-WG2-2 | IFIP-LNCS-10522 | IFIP-LNCS

Citation

Gianluca Barbon, Vincent Leroy, Gwen Salaün. Debugging of Concurrent Systems using Counterexample Analysis. Mehdi Dastani; Marjan Sirjani. 7th International Conference on Fundamentals of Software Engineering (FSEN), Apr 2017, Tehran, Iran. Springer Verlag, Lecture Notes in Computer Science, LNCS-10522, pp.20-34, 2017, Fundamentals of Software Engineering. 〈http://fsen.ir/2017/〉. 〈10.1007/978-3-319-68972-2_2〉. 〈hal-01533401v2〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

285

Téléchargements de fichiers

54

Contact


archive-ouverte@inria.fr