| UML状态机到B形式化规约的转换 |
| |
| 引用本文： | 肖健宇,张德运,董皓,陈海诠.UML状态机到B形式化规约的转换[J].微电子学与计算机,2005,22(8):80-84. |
| |
| 作者姓名： | 肖健宇 张德运 董皓 陈海诠 |
| |
| 作者单位： | 1. 西安交通大学电子与信息工程学院,陕西,西安,710049;邵阳学院,湖南,邵阳,422000
2. 西安交通大学电子与信息工程学院,陕西,西安,710049 |
| |
| 基金项目： | 国家863网络安全管理与测评技术（8633010503） |
| |
| 摘 要： | 文章研究在高可信软件工程中集成形式化方法。以软件设计的UML状态机模型为起点．将其转换为B形式化模型，然后在B工具环境中遵循B方法的精化原则和正确性验证方法，开发出可靠的实现模型。提出一套从UML状态机到B形式化规约的转换规则，涵盖UML基本状态图、分层状态图和并发状态图。实例分析表明．这套转换规则行之有效。
|
| 关 键 词： | UML状态机 形式化方法 B方法 高可信软件工程 |
| 文章编号： | 1000-7180（2005）08-080-05 |
| 收稿时间： | 2005-01-05 |
| 修稿时间： | 2005年1月5日 |
Transformation From UML State Machine to B Formal Specification |
| |
| XIAO Jian-yu,ZHANG De-yun,DONG Hao,CHEN Hai-quan.Transformation From UML State Machine to B Formal Specification[J].Microelectronics & Computer,2005,22(8):80-84. |
| |
| Authors: | XIAO Jian-yu ZHANG De-yun DONG Hao CHEN Hai-quan |
| |
| Abstract: | Integration of formal method into high-confidence software engineering was studied. The UML state machine of software design model was first transformed into B formal specification. Then, in the B tool kit environment, the reliable implementation model was developed according to the refinement principle of B method and its correctness verification facility. A suit of transformation rules from UML state machine into B formal model were proposed, including UML basic state diagram, hierarchical state diagram and concurrent state diagram. Experiment showed that the proposed transformation rules were practical. |
| |
| Keywords: | UML state machine Formal method B-method High-confidence software engineering |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
