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

doi:“863”国家高技术研究发展计划基金资助项

吉林大学学报(工学版)

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

肖健宇¹,²，张德运¹，陈海诠¹，董浩¹

1.西安交通大学电子与信息工程学院，西安 710049； 2.邵阳学院计算机系，湖南邵阳 422000

收稿日期:2005-04-08 修回日期:2005-07-13 出版日期:2005-09-01 发布日期:2005-09-01
通讯作者: 张德运

Development and Verification of High Confidence Embedded Software

XIAO Jian-yu¹,², ZHANG De-yun¹, CHEN Hai-quan¹, DONG Hao¹

1.College of Electronics and Information Engineering, Xi'an Jiaotong University, Xi'an 710049, China; 2.Department of Computer Science, Shaoyang University, Shaoyang 422000, China

Received:2005-04-08 Revised:2005-07-13 Online:2005-09-01 Published:2005-09-01
Contact: ZHANG De-yun1

摘要/Abstract

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

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

Abstract: UML state machine model of software was transformed into the input language of model checker MOCHA and was checked in it. The model checker gave counterexamples path according to the flaw found in the model checked, which could modify the software UML design model. The verified UML model was transformed into abstract specifications of B method, in which it can be refined, verified and translated into source C code. The rules of transformation from UML state machine to REACTIVE MODULES modelling language and B AMN abstract specifications were put forward. The experimental result shows that the strategy could significantly improves the efficiency of development and verification of highconfidence embedded software.

Key words: computer software, model checking, theorem proving, highconfidence software, software verification, MOCHA, B method

中图分类号:

TP311.1

肖健宇,，张德运，陈海诠，董浩. 模型检测与定理证明相结合开发并验证高可信嵌入式软件[J]. 吉林大学学报(工学版), 2005, 35(05): 531-0536.

XIAO Jian-yu,, ZHANG De-yun, CHEN Hai-quan, DONG Hao. Development and Verification of High Confidence Embedded Software[J]. 吉林大学学报(工学版), 2005, 35(05): 531-0536.

参考文献

相关文章 15

[1]	马健, 樊建平, 刘峰, 李红辉. 面向对象软件系统演化模型[J]. 吉林大学学报(工学版), 2018, 48(2): 545-550.
[2]	罗养霞, 郭晔. 基于数据依赖特征的软件识别[J]. 吉林大学学报(工学版), 2017, 47(6): 1894-1902.
[3]	应欢, 王东辉, 武成岗, 王喆, 唐博文, 李建军. 适用于商用系统环境的低开销确定性重放技术[J]. 吉林大学学报(工学版), 2017, 47(1): 208-217.
[4]	李勇, 黄志球, 王勇, 房丙午. 基于多源数据的跨项目软件缺陷预测[J]. 吉林大学学报(工学版), 2016, 46(6): 2034-2041.
[5]	王念滨, 祝官文, 周连科, 王红卫. 支持高效路径查询的数据空间索引方法[J]. 吉林大学学报(工学版), 2016, 46(3): 911-916.
[6]	陈鹏飞, 田地, 杨光. 基于MVC架构的LIBS软件设计与实现[J]. 吉林大学学报(工学版), 2016, 46(1): 242-245.
[7]	特日跟, 江晟, 李雄飞, 李军. 基于整数数据的文档压缩编码方案[J]. 吉林大学学报(工学版), 2016, 46(1): 228-234.
[8]	康辉, 王家琦, 梅芳. 基于Pi演算的并行编程语言[J]. 吉林大学学报(工学版), 2016, 46(1): 235-241.
[9]	刘磊, 王燕燕, 申春, 李玉祥, 刘雷. Bellman-Ford算法性能可移植的GPU并行优化[J]. 吉林大学学报(工学版), 2015, 45(5): 1559-1564.
[10]	冯晓宁, 王卓, 张旭. 基于L-π演算的WSN路由协议形式化方法[J]. 吉林大学学报(工学版), 2015, 45(5): 1565-1571.
[11]	李明哲, 王劲林, 陈晓, 陈君. 基于网络处理器的流媒体应用架构模型(VPL)[J]. 吉林大学学报(工学版), 2015, 45(5): 1572-1580.
[12]	王克朝, 王甜甜, 苏小红, 马培军. 基于频繁闭合序列模式挖掘的学生程序雷同检测[J]. 吉林大学学报(工学版), 2015, 45(4): 1260-1265.
[13]	黄宏涛，王静，叶海智，黄少滨. 基于惰性切片的线性时态逻辑性质验证[J]. 吉林大学学报(工学版), 2015, 45(1): 245-251.
[14]	范大娟^{1, 2}, 黄志球¹, 肖芳雄¹, 祝义¹, 王进¹. 面向多服务交互的相容性分析与适配器生成[J]. 吉林大学学报(工学版), 2014, 44(4): 1094-1103.
[15]	贺秦禄¹, 李战怀¹, 王乐晓¹, 王瑞². 云存储系统聚合带宽测试技术[J]. 吉林大学学报(工学版), 2014, 44(4): 1104-1111.

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed

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

Development and Verification of High Confidence Embedded Software

PDF (PC)

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

Metrics

本文评价

推荐阅读 0