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

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

Abstract: A practical scheme integrating UML state machine and B method to develop reliable embedded software is proposed. The UML state machine model of software is first translated into B abstract model whose consistency is verified in B tool; then in the environment of B method, the verified abstract model is refined step by step into implementation model and finally translated into source C code with the aid of B toolkit. The correctness of the abstract model and of the refinement process is guaranteed by the B method. Experiment shows that this scheme strategically combines the advantages of UML’s intuitionism and B method’s rigor and can effectively improve the development and verification of high-confidence embedded software. The rules of transforming from UML state machine into B abstract machine are provided.

Key words: Bmethod; Formal method; UML state machine; Embedded software; High-confidence software engineering