Abstract: Statecharts that extends the finite state machine is a visual language for specifying the behavior of complex reactive system. The state of timed Statecharts is represented by inductive term from kind of term algebra, and a step semantics of timed Statecharts is briefly introduced. Based on process algebra, this paper discusses concurrent behavior for Statecharts by concurrent interleaving sequences. It describes a compositional approach for formalizing the Statecharts semantics directly on sequences of micro steps using labeled transition systems as semantics domain. The results suggest that a concise compositional semantics of timed Statecharts is basal and helpful for model checking Statecharts.

Key words: Statecharts, Operation semantics, Labeled transition systems(LTS)

摘要： Statecharts是一种用于复杂反应式系统行为的可视化规格语言。该文提出了一种基于标签变迁系统(LTS)的Statecharts操作语义描述方法，介绍了Statecharts及其项语法和一步语义，并基于进程代数描述Statecharts的并发行为，使用结构化的操作语义SOS规则描述Statecharts的组合语义，从而得到相应的LTS。

关键词: Statecharts, 操作语义, 标签变迁系统

CLC Number: 

• TP301