ISSN : 1796-217X
Volume : 4    Issue : 3    Date : May 2009

Efficient Algorithms for Verification of UML Statechart Models
C.M. Prashanth and K. Chandrashekhar Shet
Page(s): 175-182
Full Text:
PDF (516 KB)

In this article, we present algorithms devised for the automatic verification of UML(Unified Modeling
Language) statechart models. The basic algorithm checks the safety property violation during the
construction (on-the-fly) of the state space graph and if any property violation is found, it generates a
counter example. The second algorithm builds the state space considering only those events,
which could lead to the negative behavior of the system. In other words, a set of relevant events is
generated first and state space is constructed considering only the state transitions of the objects
caused by these relevant events. Thus search space is reduced in both the methods. As a case
study, we have verified UML statechart model of the Generalized Railroad Crossing (GRC) system
using the proposed algorithms. The safety property “When the train is at rail road crossing, the gate
always remain closed” is verified. We could detect property violation in the initial UML statechart
model of GRC and eventually it is corrected with the help of the counter example generated by the
algorithms. The case study results show that event based verification algorithm yields 59%
reduction in the state space for the GRC example.

Index Terms
Software verification, Model checking, Statechart, Unified Modeling Language, Reactive systems