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

摘要：

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

关键词：B方法、形式化方法、UML状态机、嵌入式软件、高可信软件工程

所属期刊栏目：32

分类号：TP311.1(计算技术、计算机技术)

资助基金：国家科技攻关项目863-301-05-03

在线出版日期：2006-05-18（万方平台首次上网日期，不代表论文的发表时间）

页数：共3页

页码：64-66