The Compositional Semantics of Timed Statecharts

J. Qian and B. Xu (PRC)


Timed Statecharts, TLTS, Operation semantic


Timed Statecharts is an extension to the visual specification language Statecharts with real-time constructs, and efficiently specify explicit dense time. The paper firstly defines timed Statecharts that extends to specify explicit continued time, such as clock constraint of timed automata. Then the state of timed Statecharts is represented by inductive term from a kind of term algebra, and a-step semantics of timed Statecharts is briefly introduced. Finally, this paper describes a compositional approach for formalizing the timed Statecharts semantics directly on sequences of micro steps by using timed labeled transition systems as semantics domain. The results suggest that a concise compositional semantics of timed Statecharts is basic and helpful for model checking timed Statecharts.

Important Links:

Go Back