A New approach to Detect Safety Violations in UML Statechart Models

The model based development is a widely accepted phenomenon to build reliable software. This has prompted development of tools capable of generating code from the model. Such rapid software development tools are handy in development of embedded systems. The code generated using tools can be deployed directly on to target hard ware, provided the model correctness is ensured. In this paper, we present an efficient procedure to verify UML (Unified Modeling Language) statechart models of reactive and concurrent systems. The algorithm checks for safety property violation during the construction (on-the-fly) of the state space graph and generates counter example if any violation is found. The exploration of the state space is terminated, as soon as safety violation is found and hence search space is reduced. We prove the correctness of the approach by taking a benchmark case study of Generalized Railroad Crossing (GRC) system. The dynamic behavior of the gate & track, two concurrent objects of the GRC system are modeled using UML statecharts and the safety property "when train is at the crossing, the gate always remain closed" is verified. We could detect property violation in the initial UML statechart model of GRC and later it is corrected with the help of the counter example generated by the algorithm. The case study results show that the verification algorithm yields 13% reduction in the state space for the GRC example.