Formal modeling and analysis of UML statecharts

The structural and semantic features of UML statecharts are analyzed firstly, and the hierarchical colored Petri net(HCPN) is constructed to solve modeling issues,especially those related to hierarchical statecharts with composite states. The Petri subnet for a composite state is composed of input/output interfaces, a state-transition part and a history state part. The input/output interfaces are used to parse entry arcs and gather exiting arcs to/from composites respectively. The state-transition part realizes transitions of the internal states. The history state part deals with memory recovery and memory cleanup of history units. After abstracting semantic rules and constrains of entry/exit transitions, their descriptions and analysis techniques of composite states based on HCPNs are illustrated. Finally, in the view of safety of UML statechart, HCPN semantic representation for completeness, consistency and reachability of statechart is elaborated. Optimizing the design of complex systems the guide in theory and practice for further research on developing automatic verification tools is provided.