Study on Operation Semantics of Statecharts Based on LTS
Lingzhong Zhao · Jisuanji gongcheng · 2006
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.