Consistency checking of behavioural modeling in UML statechart diagrams

The UML statechart diagram is widely used modeling language for describing behavioural aspect of software systems. Its rich notions of structurization make the description brief but difficult to be well-defined and consistent with the describer's intention. We present a procedure to check the validity of UML statechart diagrams. The procedure checks the existence of conflicting transitions, inappropriate history indicators, inappropriate complete transitions and dead states while constructing model graphs of UML statechart diagrams for LTL model checking. These checks contribute to removal of both ambiguous and undefined descriptions of the behaviour. After the construction of the well-defined model, the procedure executes model checking with specifications written in LTL for the consistency between the behaviour of the system and the describer's intention.