Affordable Access

Clusters of Faulty States for Debugging Behavioural Models

Authors
  • Faqrizal, Irman
  • Salaün, Gwen
Publication Date
Dec 02, 2020
Source
Hal-Diderot
Keywords
Language
English
License
Unknown
External links

Abstract

Designing and developing distributed software hasalways been a tedious and error-prone task, and the ever increasingsoftware complexity is making matters even worse. Modelchecking is an established technique for automatically findingbugs by verifying that a model satisfies a given temporal property.When the model violates the property, the model checker returnsa counterexample, which is a sequence of actions leading toa state where the property is not satisfied. Understanding thiscounterexample for debugging the specification or program is acomplicated task because the counterexample gives only a partialview of the source of the problem, and because there is usuallylittle support beyond that counterexample to identify the sourceof the problem.In this paper, we focus on behavioural models (Labelled TransitionSystems) and we propose some techniques for simplifying thedebugging of erroneous models. We first focus on the erroneouspart of the model and we detect specific states (called faultystates) where a choice is possible between executing a correctbehaviour or falling into an erroneous part of the model. Thegoal of this paper is to group these faulty states into clusters.Clusters help the user to identify the source of the bug sinceeach cluster of states provides some information about the bug.We implemented this technique into a tool, which allows thevisualization of the faulty model and the computation of clusters.

Report this publication

Statistics

Seen <100 times