Database of Research Tools Developed Using CADP

CLEAR

Organisation: Université Grenoble Alpes, Laboratoire d'Informatique de Grenoble (FRANCE)

Functionality: Summarisation of counterexamples provided by a model checker

Tools used: CADP (Construction and Analysis of Distributed Processes)
Jung (Java Universal Network/Graph Framework) library
Neo4j graph database

Period: 2015-2020

Description: Model checking is a powerful technique to detect the presence of bugs in a model. In the case of a bug, the model checker provides a counterexample, which is most of the time given to the human designer to correct the model. However, understanding this counterexample is not always obvious, because the counterexample might be large and does not point explicitely to the source of the bug, for instance by highlighting the most relevant actions.

The CLEAR tool provides several features to assist in the understanding a counterexample. First, CLEAR provides modules to compute the states (called neighbourhoods) that contain a choice between a correct and incorrect behaviour. For this, CLEAR provides two different techniques. The first technique is based on inspecting the difference between the model and the LTS containing all counterexamples; this technique is suited for properties where all counterexamples are traces, e.g., safety properties. The second technique is based on the computation of common prefixes and suffixes, and can be applied to properties containing cycles, e.g., liveness properties. Secondly, CLEAR provides a 3D visualisation module, which highlights the neighbourhoods, providing a global view of the bug in the model.

CLEAR relies on CADP for the modeling of the system, model checking, and counterexample generation. More precisely, the system is considered to be provided as an LNT model, which is then translated into an LTS in AUT or BCG format. The properties are specified in MCL, and model checked using EVALUATOR. To compute the LTS containing all counterexamples, CLEAR uses an SVL script that successively calls EVALUATOR (to generate an LTS corresponding to the formula), EXP.OPEN (to compute the product of the model and the property), REDUCTOR (to reduce the LTS), and SCRUTATOR (to remove spurious traces).

Conclusions: The modularity and well documented interfaces of CADP ease the development of companion tools that help designers understand the verification results.

Publications: [Barbon-Leroy-Salaun-17] Gianluca Barbon, Vincent Leroy, and Gwen Salaün. "Debugging of Concurrent Systems using Counterexample Analysis". Proceedings of the 7th IPM International Conference on Fundamentals of Software Engineering (FSEN 2017), Tehran, Iran, Notes in Computer Science, volume 10522, pages 20-34, Springer, April 2017.
Available on-line at: http://convecs.inria.fr/doc/publications/Barbon-Leroy-Salaun-17.pdf
or from the CADP Web site in PDF or PostScript

[Barbon-Leroy-Salaun-18] Gianluca Barbon, Vincent Leroy, and Gwen Salaün. "Counterexample Simplification for Liveness Property Violation". Proceedings of the 16th International Conference on Software Engineering and Formal Methods (SEFM 2018), Toulouse, France, Lecture Notes in Computer Science, volume 10886, pages 173-188, Springer, June 2018.
Available on-line at: http://convecs.inria.fr/doc/publications/Barbon-Leroy-Salaun-18.pdf
or from the CADP Web site in PDF or PostScript

[Barbon-18] Gianluca Barbon. "Debugging of Behavioural Models using Counterexample Analysis". PhD thesis, Université Grenoble Alpes, December 2018.
Available on-line at: https://tel.archives-ouvertes.fr/tel-02191544/en
or from the CADP Web site in PDF or PostScript

[Faqrizal-Salaun-20] Irman Faqrizal and Gwen Salaün. "Clusters of Faulty States for Debugging Behavioural Models". Proc. of the 27th Asia-Pacific Software Engineering Conference (APSEC'2020), Singapore, December 1-4, 2020.
Available on-line at: https://hal.inria.fr/hal-03035539/en
or from the CADP Web site in PDF or PostScript

[Barbon-Leroy-Salaun-21] Gianluca Barbon, Vincent Leroy, and Gwen Salaün. "Debugging of Behavioural Models using Counterexample Analysis". IEEE Transactions on Software Engineering 47(6):1184-1197, 2021.
Available on-line at: http://hal.inria.fr/hal-02145610/en
or from the CADP Web site in PDF or PostScript

Contact:
Gwen Salaün
Inria Grenoble - Rhône-Alpes / CONVECS
655 Avenue de l'Europe
38330 Montbonnot Saint-Martin
France
Email: Gwen.Salaun at inria.fr
Further remarks: This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software

Last modified: Fri Mar 25 14:31:39 2022.

Back to the CADP research tools page