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

摘要

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