摘要: 给出了Statecharts的抽象语法描述,以及Statecharts各个构成元素的语义,包括状态、迁移、事件和条件、表达式、动作和当前状态格局的语义函数等,并给出Statecharts一步的操作语义。然后在此基础上把一个图形化的语言转换为文本的方式来描述,并对Statecharts进行形式化分析及验证。
关键词:
Statecharts,
抽象语法,
操作语义,
一步
Abstract: The Statecharts is represented as an abstract syntax intend to hide these details in presentation of the semantics,and compositive aspects of the semantics of Statecharts are discussed,including state,transition,event,condition,expression,action and state configuration.Based on compositive semantics of Statecharts,operation semantics of a macro step is given.Graphic Statecharts is translated into text language for verifying syntax's correctness and semantics' legitimacy.
中图分类号:
钱俊彦,古天龙,赵岭忠. Statecharts的形式化验证研究[J]. , 2005, 31(18): 29-.
QIAN Junyan,GU Tianlong,ZHAO Lingzhong. Formal Verification for Statecharts[J]. , 2005, 31(18): 29-.