In: Information and Software Technology, Vol. 36, No. 10, pages 615-624. 1994.
Abstract: Statecharts are an extension to finite state machines with capability for expressing hierarchical decomposition and parallelism. They also have a mechanism called history, to remember the last visit to a superstate. An algorithm to create a reachability tree for statecharts is presented. Also shown is how to use this tree to analyze dynamic properties of statecharts; reachability from any state configuration, usage of transitions, reinitiability, deadlocks, and valid sequence of events. Owing to its powerful notation, building a reachability tree for statecharts presents some difficulties, and we show how these problems were solved in the tree we propose.
Keywords: Petri nets, exhaustive simulation, reachability trees, reactive systems, statecharts.