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-2022

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).

CLEAR was extended with new functionalities for computing clusters of faulty states denoting the same erroneous portion of the LTS and for counting the number of bugs in the original specification by modifying the specification and of analyzing the changes in the LTS.

Conclusions: The modularity and well documented interfaces of CADP ease the development of companion tools that help designers understand the verification results. The CLEAR tool provides useful functionalities assisting the debugging of concurrent systems.

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

[Barbon-Leroy-Salaun-19] Gianluca Barbon, Vincent Leroy, and Gwen Salaün. "Debugging of Behavioural Models with CLEAR". Proc. of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'2019), Prague, Czech Republic, Lecture Notes in Computer Science vol. 11427, pp. 386-392. Springer Verlag, April 2019.
Available on-line at: https://hal.inria.fr/hal-02121180/en
or from the CADP Web site in PDF or PostScript

[Barbon-Leroy-Salaun-Yah-19] Gianluca Barbon, Vincent Leroy, Gwen Salaün, and Emmanuel Yah. "Visual Debugging of Behavioural Models". Proc. of the 41st ACM/IEEE International Conference on Software Engineering (ICSE'2019), Montréal, Canada, pp. 107-110.
Available on-line at: https://inria.hal.science/hal-02145535/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

[Faqrizal-Salaun-22] Irman Faqrizal and Gwen Salaün. "Counting Bugs in Behavioural Models using Counterexample Analysis". Proc. of the 10th International Conference on Formal Methods in Software Engineering (FormaliSE'2022), Pittsburgh, PA, pp. 12-22. IEEE/ACM, May 2022.
Available on-line at: http://hal.inria.fr/hal-03665317/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 Feb 23 09:45:26 2024.

Back to the CADP research tools page