Skip to Main content Skip to Navigation
New interface
Conference papers

Counterexample Simplification for Liveness Property Violation

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 techniques verify 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 because the developer has to understand by manual analysis all the steps (possibly many) that have provoked the bug. The objective of this work is to improve the comprehension of counterexamples and thus to simplify the detection of the source of the bug. Given a liveness property, our approach first extends the model with prefix / suffix information w.r.t. that property. This enriched model is then analysed to identify specific states called neighbourhoods. A neighbourhood consists of a choice between transitions leading to a correct or incorrect part of the model. We exploit this notion of neighbourhood to highlight relevant parts of the counterexample, which makes easier its comprehension. Our approach is fully automated by a tool that we implemented and that was validated on several real-world case studies.
Complete list of metadata

Cited literature [18 references]  Display  Hide  Download
Contributor : Gianluca Barbon Connect in order to contact the contributor
Submitted on : Tuesday, June 19, 2018 - 3:26:12 PM
Last modification on : Wednesday, July 6, 2022 - 4:19:37 AM
Long-term archiving on: : Tuesday, September 25, 2018 - 7:23:35 AM


Files produced by the author(s)



Gianluca Barbon, Vincent Leroy, Gwen Salaün. Counterexample Simplification for Liveness Property Violation. SEFM 2018 - 16th International Conference on Software Engineering and Formal Methods, Jun 2018, Toulouse, France. pp.173-188, ⟨10.1007/978-3-319-92970-5_11⟩. ⟨hal-01818790⟩



Record views


Files downloads