Model checking for timed statecharts

Abstract

Timed Statecharts, which can efficiently specify explicit dense time, is an extension to the visual specification language Statecharts with real-time constructs. We give a definition of timed Statecharts that specifies explicit temporal behavior as timed automata does. It is very difficult to verify directly whether timed Statecharts satisfies the required properties. However, by compiling it into timed automata, timed Statecharts may be checked using UPPAAL tool. In the paper, the state of timed Statecharts is represented by inductive term, and a step semantics of timed Statecharts is briefly described. The translation rules are shown by a compositional approach for formalizing the timed Statecharts semantics directly on sequences of micro steps. Timed automata corresponding to timed Statecharts was also discussed. © IFIP International Federation for Information Processing 2005.