Model checking UML statecharts

Unified Modeling Language (UML) has been widely used in software development. Verifying if an UML model meets the required properties has become a key issue. Model checking is an important technology of automatic formal verification to ensure the correctness of design specifications. An approach of model checking UML statecharts is given in this paper At first, the brief syntax and semantics of UML statecharts are described. Then, the way of how UML statecharts is structurally expressed by extended hierarchical automaton and the labeled transition system are defined. The correctness of operational semantics of UML statecharts can be ensured through finding the maximal non-conflict transition set. For the system with infinite runs, the operational semantics can be mapped to a Buchi automaton and linear temporal logic properties of the system can be verified based on the automata theory of model checking. The paper also presents the method of verifying complex system consist of multiple objects modeled by statecharts and collaboration diagram.