Skip to Main content Skip to Navigation
Conference papers

Clusters of Faulty States for Debugging Behavioural Models

Irman Faqrizal 1 Gwen Salaün 1
1 CONVECS - Construction of verified concurrent systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : Designing and developing distributed software has always been a tedious and error-prone task, and the ever increasing software complexity is making matters even worse. Model checking is an established technique for automatically finding bugs by verifying that a model satisfies a given temporal property. When the model violates the property, the model checker returns a counterexample, which is a sequence of actions leading to a state where the property is not satisfied. Understanding this counterexample for debugging the specification or program is a complicated task because the counterexample gives only a partial view of the source of the problem, and because there is usually little support beyond that counterexample to identify the source of the problem. In this paper, we focus on behavioural models (Labelled Transition Systems) and we propose some techniques for simplifying the debugging of erroneous models. We first focus on the erroneous part of the model and we detect specific states (called faulty states) where a choice is possible between executing a correct behaviour or falling into an erroneous part of the model. The goal of this paper is to group these faulty states into clusters. Clusters help the user to identify the source of the bug since each cluster of states provides some information about the bug. We implemented this technique into a tool, which allows the visualization of the faulty model and the computation of clusters.
Complete list of metadatas

https://hal.inria.fr/hal-03035539
Contributor : Gwen Salaün <>
Submitted on : Wednesday, December 2, 2020 - 11:27:32 AM
Last modification on : Thursday, December 3, 2020 - 1:21:40 PM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-03035539, version 1

Collections

Citation

Irman Faqrizal, Gwen Salaün. Clusters of Faulty States for Debugging Behavioural Models. APSEC 2020 - 27th Asia-Pacific Software Engineering Conference, Dec 2020, Singapore, Singapore. pp.1-9. ⟨hal-03035539⟩

Share

Metrics

Record views

53

Files downloads

59