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

摘要：首先将软件的UML状态机模型转换为模型检测工具MOCHA的输入语言REACTIVEMODULES,在MOCHA中进行正确性验证,利用模型检测工具针对错误情况给出的反例路径,尽早修改软件的UML设计模型;然后将已验证过的UML模型转换为定理证明工具B方法的抽象规约,利用B方法的精化、验证及代码生成功能,直接生成正确的C代码。并给出了从UML状态机到REACTIVE MODULES建模语言及B AMN抽象规约的转换规则。实验结果表明,该方法可在软件工程中有效地提高高可信嵌入式软件开发和验证的效率。

摘要：文章研究在高可信软件工程中集成形式化方法。以软件设计的UML状态机模型为起点,将其转换为B形式化模型,然后在B工具环境中遵循B方法的精化原则和正确性验证方法,开发出可靠的实现模型。提出一套从UML状态机到B形式化规约的转换规则,涵盖UML基本状态图、分层状态图和并发状态图。实例分析表明,这套转换规则行之有效。