Skip to Main content Skip to Navigation
Journal articles

Debugging of Behavioural Models 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 [Grenoble]
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 a large number of actions, (ii) the debugging task is mostly achieved manually, and (iii) the counterexample does not explicitly highlight the source of the bug that is hidden in the model. This article presents a new approach that improves the usability of model checking by simplifying the comprehension of counterexamples. To do so, we first extract in the model all the counterexamples. Second, we define an analysis algorithm that identifies actions that make the model skip from incorrect to correct behaviours, making these actions relevant from a debugging perspective. Third, we develop a set of abstraction techniques to extract these actions from counterexamples. Our approach is fully automated by a tool we implemented and was applied on real-world case studies from various application areas for evaluation purposes.
Document type :
Journal articles
Complete list of metadata

Cited literature [32 references]  Display  Hide  Download
Contributor : Gwen Salaün Connect in order to contact the contributor
Submitted on : Monday, June 3, 2019 - 10:38:55 AM
Last modification on : Thursday, October 21, 2021 - 3:45:24 AM


Files produced by the author(s)



Gianluca Barbon, Vincent Leroy, Gwen Salaün. Debugging of Behavioural Models using Counterexample Analysis. IEEE Transactions on Software Engineering, Institute of Electrical and Electronics Engineers, 2021, 47 (6), pp.1184-1197. ⟨10.1109/TSE.2019.2915303⟩. ⟨hal-02145610⟩



Les métriques sont temporairement indisponibles