Slicing UML Statecharts for Model Checking
Zhichang Qi · Dianzi xuebao · 2002
Unified Modeling Language (UML) has been widely used in software development. Verifying whether a UML model meets the reared properties has become a challenge. Model checking is an important technology of automatic verification to ensure the correctness of designed models. Because of space explosion and complicated semantics, model checking Statecharts are restricted by the software scale and the refinement degree of design. In this paper, UML Statecharts are structurally expressed by Extended Hierarchical Automaton (EHA). A set of dependence relations is specified after analyzing the characteristics such as hierarchy, concurrency and synchronization in EHA. The algorithm of slicing EHA based on the slicing criterion which is composed by states and transitions is presented. The sliced EHA and the original Statecharts are equivalent to the property.The algorithm removes the hierarchies and concurrent states which are irrelevant with the property, and reduce the state space efficiently.