模型检测与定理证明相结合开发并验证高可信嵌入式软件

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