A REACHABILITY TREE FOR STATECHARTS AND ANALYSIS OF SOME PROPERTIES - Masiero, P. C.; Maldonado, J. C.; Boaventura, I. G. (Butterworth-heinemann Ltd, 1994)
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 analyse 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: STATECHARTS; REACTIVE SYSTEMS; REACHABILITY TREE; EXHAUSTIVE SIMULATION; DYNAMIC PROPERTIES OF STATECHARTS