Paper Info
Title
Clusters of Faulty States for Debugging Behavioural Models
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.
Year
DOI
Venue
2020
10.1109/APSEC51365.2020.00017
2020 27th Asia-Pacific Software Engineering Conference (APSEC)
Keywords
DocType
ISSN
behavioural models,model checking,debugging,Internet of Things
Conference
1530-1362
ISBN
Citations 
PageRank 
978-1-7281-9554-4
1
0.36
References 
Authors
0
2
Name
Order
Citations
PageRank
Irman Faqrizal110.36
Gwen Salaün298871.03