Simulation and verification tool for hierarchical real-time systems

The computerized tool for statecharts based modeling and simulation of reactive systems with timing constraints is described in the paper. GUI enables to draw and edit the statecharts, and to specify the required behavior of the system. Useful types of properties, such as state reachability, safety, and response, can be specified and verified. The model-checking algorithm for statecharts verification works without constructing the flat state-transition graph. If the required property does not hold in the system, the counter-example can be found without searching the whole state space.