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.
Origin : Files produced by the author(s)