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

摘要：

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

关键词：计算机软件、模型检测、定理证明、高可信软件、软件正确性验证、MOCHA、B方法

所属期刊栏目：35

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

资助基金：国家高技术研究发展计划863计划863-301-05-03

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

页数：共6页

页码：531-536