| 基于UML状态机与B方法的高可信嵌入式软件开发 |
| |
| 引用本文： | 肖健宇,张德运,陈海诠,董皓.基于UML状态机与B方法的高可信嵌入式软件开发[J].计算机工程,2006,32(8):64-66. |
| |
| 作者姓名： | 肖健宇 张德运 陈海诠 董皓 |
| |
| 作者单位： | 1. 湖南涉外经济学院计算机系,长沙,410205;西安交通大学电子与信息工程学院,西安,710049
2. 西安交通大学电子与信息工程学院,西安,710049 |
| |
| 摘 要： | 提出了一套集成UML与B方法开发高可信嵌入式软件的实用方案：以软件的UML状态机模型为起点，将其转换为B抽象模型并在B工具中验证该模型的一致性，然后遵循B模型逐步精化的开发规则，利用B方法的精化正确性验证功能，得到系统的可靠的实现模型，最后借助B工具自动生成C代码。实例分析表明，这套方法可以提高尚可信嵌入式软件的开发验证效率。给出了嵌入式软件设计中常用的UML并发状态图到B抽象模型的转换规则。
|
| 关 键 词： | B方法 形式化方法 UML状态机 嵌入式软件 高可信软件工程 |
| 文章编号： | 1000-3428（2006）08-0064-13 |
| 收稿时间： | 05 25 2005 12:00AM |
| 修稿时间： | 2005-05-25 |
High-confidence Embedded Software Development Based on UML State Machine and B Method |
| |
| XIAO Jianyu,ZHANG Deyun,CHEN Haiquan,DONG Hao.High-confidence Embedded Software Development Based on UML State Machine and B Method[J].Computer Engineering,2006,32(8):64-66. |
| |
| Authors: | XIAO Jianyu ZHANG Deyun CHEN Haiquan DONG Hao |
| |
| Abstract: | |
| |
| Keywords: | Bmethod Formal method UML state machine Embedded software High-confidence software engineering |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
