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 ![]() ![]() [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 ![]() ![]() [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 ![]() ![]() [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 ![]() ![]() [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 ![]() ![]() |
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 |