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

https://hal.archives-ouvertes.fr/hal-02121180
Contributor : Radu Mateescu <>
Submitted on : Wednesday, May 15, 2019 - 8:21:46 AM
Last modification on : Wednesday, May 15, 2019 - 8:23:28 AM

File

Barbon2019_Chapter_DebuggingOf...
Files produced by the author(s)

Identifiers

Citation

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⟩

Share

Metrics

Record views

69

Files downloads

7