基于UML状态机与B方法的高可信嵌入式软件开发

• 作者: 张德运 肖健宇 董皓 陈海诠
• 来源期刊: 计算机工程
• 学科: 工学
• 关键词: B方法 形式化方法 UML状态机 嵌入式软件 高可信软件工程
• 年，卷（期）: 2006,（8）
• 所属期刊栏目: 软件技术与数据库
• 页码范围: 64-66
• 页数: 3页
• 分类号: TP311.1
• 字数: 2624字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-3428.2006.08.023

摘要

提出了一套集成UML与B方法开发高可信嵌入式软件的实用方案:以软件的UML状态机模型为起点,将其转换为B抽象模型并在B工具中验证该模型的一致性,然后遵循B模型逐步精化的开发规则,利用B方法的精化正确性验证功能,得到系统的可靠的实现模型,最后借助B工具自动生成C代码.实例分析表明,这套方法可以提高高可信嵌入式软件的开发验证效率.给出了嵌入式软件设计中常用的UML并发状态图到B抽象模型的转换规则.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张德运	西安交通大学电子与信息工程学院	184	2190	23.0	37.0
2	肖健宇	湖南涉外经济学院计算机系	4	21	2.0	4.0
6	陈海诠	西安交通大学电子与信息工程学院	8	67	5.0	8.0
7	董皓	西安交通大学电子与信息工程学院	12	83	6.0	9.0