An Efficient Event Based Approach for Verification of UML Statechart Model for Reactive Systems

This paper describes an efficient method to detect safety specification violations in dynamic behavior model of concurrent/reactive systems. The dynamic behavior of each concurrent object in a reactive system is assumed to be represented using UML (Unified Modeling Language) statechart diagram. The verification process involves building a global state space graph from these independent statechart diagrams and traversal of large number of states in global state space graph for detecting a safety violation. In our approach, a safety property to be verified is read first and a set of events, which could violate this property, is computed from the model description. We call them as "relevant events". The global state space graph is constructed considering only state transitions caused by the occurrence of these relevant events. This method reduces the number of states to be traversed for finding a property violation. Hence, this technique scales well for complex reactive systems. As a case study, the proposed technique is applied to verification of Generalized Railroad Crossing (GRC) system and safety property "When train is at railroad crossing, the gate always remain closed" is checked. We could detect a flaw in the infant UML model and eventually, correct model is built with the help of counter example generated. The result of the study shows that, this technique reduces search space by 59% for the GRC example.