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

• 作者: 张德运 肖健宇 董浩 陈海诠
• 来源期刊: 吉林大学学报（工学版）
• 学科: 工学
• 关键词: 计算机软件 模型检测 定理证明 高可信软件 软件正确性验证 MOCHA B方法
• 年，卷（期）: 2005,（5）
• 页码范围: 531-536
• 页数: 6页
• 分类号: TP311.1
• 字数: 3507字
• 语种: 中文
• DOI: 10.3969/j.issn.1671-5497.2005.05.015

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张德运	西安交通大学电子与信息工程学院	184	2190	23.0	37.0
2	肖健宇	西安交通大学电子与信息工程学院	13	83	6.0	8.0
4	陈海诠	西安交通大学电子与信息工程学院	8	67	5.0	8.0
7	董浩	西安交通大学电子与信息工程学院	1	12	1.0	1.0