Debugging of Behavioural Models with CLEAR

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
Abstract : This paper presents a tool for debugging behavioural models being analysed using model checking techniques. It consists of three parts: (i) one for annotating a behavioural model given a temporal formula , (ii) one for visualizing the erroneous part of the model with a specific focus on decision points that make the model to be correct or incorrect, and (iii) one for abstracting counterexamples thus providing an explanation of the source of the bug.
Complete list of metadatas
Contributor : Radu Mateescu <>
Submitted on : Wednesday, May 15, 2019 - 8:21:46 AM
Last modification on : Wednesday, May 15, 2019 - 8:23:28 AM


Files produced by the author(s)



Gianluca Barbon, Vincent Leroy, Gwen Salaün. Debugging of Behavioural Models with CLEAR. 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Apr 2019, Prague, Czech Republic. pp.386-392, ⟨10.1007/978-3-030-17462-0_ 26⟩. ⟨hal-02121180⟩



Record views


Files downloads