| Statecharts的形式化验证研究 |
| |
| 引用本文： | 钱俊彦,古天龙,赵岭忠.Statecharts的形式化验证研究[J].计算机工程,2005,31(18):19-21,24. |
| |
| 作者姓名： | 钱俊彦 古天龙 赵岭忠 |
| |
| 作者单位： | 桂林电子工业学院计算机系,桂林,541004 |
| |
| 基金项目： | “十五”国防预研基金资助项目;广西自然科学基金资助项目（0141046） |
| |
| 摘 要： | 给出了Statecharts的抽象语法描述,以及Statecharts各个构成元素的语义,包括状态、迁移、事件和条件、表达式、动作和当前状态格局的语义函数等,并给出Statecharts一步的操作语义.然后在此基础上把一个图形化的语言转换为文本的方式来描述,并对Statecharts进行形式化分析及验证.
|
| 关 键 词： | Statecharts 抽象语法 操作语义 一步 |
| 文章编号： | 1000-3428（2005）18-0019-03 |
| 收稿时间： | 2004-08-13 |
| 修稿时间： | 2004-08-13 |
Formal Verification for Statecharts |
| |
| QIAN Junyan,Gu Tianlong,ZHAO Lingzhong.Formal Verification for Statecharts[J].Computer Engineering,2005,31(18):19-21,24. |
| |
| Authors: | QIAN Junyan Gu Tianlong ZHAO Lingzhong |
| |
| Affiliation: | Computer Department, Guilin University of Electronic Technology, Guilin 541004 |
| |
| 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. |
| |
| Keywords: | Statecharts Abstract syntax Operation semantics Astep |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
