一种自动化模型检测ANSIC程序的实用方法

doi:10.3969/j.issn.1007130X.2010.

J4 ›› 2010, Vol. 32 ›› Issue (4): 79-82.doi: 10.3969/j.issn.1007130X.2010.

一种自动化模型检测ANSIC程序的实用方法

王大伟,张大方,缪力

（1.湖南大学计算机与通信学院，湖南长沙 410082；2.湖南大学软件学院，湖南长沙 410082）

收稿日期:2009-03-12 修回日期:2009-07-05 出版日期:2010-03-28 发布日期:2010-03-28
通讯作者: 王大伟 E-mail:js392781@126.com
作者简介:王大伟（1984-），男，江苏徐州人，硕士生，研究方向为程序验证；张大方，教授，博士生导师，CCF高级会员（40233302），研究方向为可信系统与网络、容错计算；缪力，副教授，研究方向为软件测试和程序分析。
基金资助:
国家自然科学基金资助项目（60673155）；国家“可信软件”重大研究计划资助项目（90718008）

A Practical Method for Automatically Model Checking the ANSIC Programs

WANG Dawei,ZHANG Dafang,MIAO Li

（1.School of Computer and Communications,Hunan University,Changsha 410082；2.School of Software,Hunan University,Changsha 410082,China）

Received:2009-03-12 Revised:2009-07-05 Online:2010-03-28 Published:2010-03-28
Contact: WANG Dawei E-mail:js392781@126.com

摘要/Abstract

摘要： 模型检测是一种验证有限状态系统的时序逻辑属性的形式化方法。为了利用模型检测技术，通常的办法是手工构建一个抽象模型，然而这个方法存在一些不足，如成本过高、易引入建模错误等。本文提出了一种自动化模型检测ANSIC程序的方法，并开发了模型提取工具C2Spin，它能够分析ANSIC源代码，并生成对应的PROMELA验证模型，从而显著降低了建模的开销。利用C2Spin，模型检测工具SPIN可以自动地检测使用C语言编写的应用程序中的多种错误，如死锁等。在初步实验中，依靠C2Spin生成的模型，我们发现了SPIN4.3.0的一个语义错误，以及Holzmann对两个经典互斥算法的实现程序中的活锁错误。这些结果表明，C2Spin能够帮助人们更加快速有效地测试C程序。

关键词: 形式化方法, 模型检测, 模型提取, ANSIC, PROMELA

Abstract: Model checking is a formal method for verifying the temporal logic properties of finite state systems. To use the technique, an abstract model is usually constructed by hand, but this approach has some weaknesses, for instance, the cost of modeling is considerably high and the artificial models are errorprone. In this paper, we present a practical method for model checking the ANSIC programs automatically. We built C2Spin, a model extractor which analyzes the C source code and extracts the PROMELA verification model from the source code, and thereby reduce the expense of modeling significantly. Then SPIN can detect various errors in the applications implemented in C mechanically using C2Spin, such as deadlock. In preliminary experiments, depending upon the models generated by C2Spin, we find a semantic bug in SPIN4.3.0 and similar livelocks in the implementation of two classic mutual exclusion algorithms written by Holzmann. The results show that C2Spin helps people test C programs more effectively and quickly.

Key words: formal method;model checking;model extraction;ANSIC;PROMELA

中图分类号:

TP301.2

王大伟,张大方,缪力. 一种自动化模型检测ANSIC程序的实用方法[J]. J4, 2010, 32(4): 79-82.

WANG Dawei,ZHANG Dafang,MIAO Li. A Practical Method for Automatically Model Checking the ANSIC Programs[J]. J4, 2010, 32(4): 79-82.

[1]	刘子源, 马占有, 李霞, 高滢囡, 何娜娜, 黄瑞祺. 基于模糊测度的模糊分支时态逻辑模型检测[J]. 计算机工程与科学, 2024, 46(04): 676-683.
[2]	李召恺, 马占有, 李健祥, 郭昊. 基于模糊决策过程的模糊计算树逻辑模型检测[J]. 计算机工程与科学, 2022, 44(02): 266-275.
[3]	郑小宇, 刘冬梅, 杜益宁, 周子健, 邱玫媚, 朱鸿. 模式驱动的系统安全性设计的验证[J]. 计算机工程与科学, 2020, 42(07): 1197-1207.
[4]	李凤英，杨恩乙，董荣胜. 图数据压缩技术综述[J]. 计算机工程与科学, 2020, 42(01): 89-97.
[5]	黄怿豪，冯劲草，郑寒月，缪炜恺，蒲戈光. 航空机载嵌入式控制软件需求建模的形式化工程方法[J]. 计算机工程与科学, 2019, 41(06): 1016-1025.
[6]	袁申,魏杰林,李永明. 具有多值决策过程的广义可能性计算树逻辑模型检测[J]. 计算机工程与科学, 2019, 41(01): 88-97.
[7]	钟小妹，肖美华，李伟，谌佳，李娅楠. RFID超轻量级认证协议RCIA形式化分析与改进[J]. 计算机工程与科学, 2018, 40(12): 2183-2192.
[8]	王亚鹏，雷丽晖. 基于CTL模型检测的胃腺癌核心路径形式化验证[J]. 计算机工程与科学, 2018, 40(12): 2280-2286.
[9]	雷丽晖，郭越，张延波. 可能性测度下的CTL符号化模型检测[J]. 计算机工程与科学, 2018, 40(11): 2008-2014.
[10]	陈颖1，刘冬梅1，朱鸿2，兰斌1，何娟娟1. 服务组合的代数规约[J]. 计算机工程与科学, 2018, 40(06): 1075-1083.
[11]	李娅楠，肖美华，李伟，梅映天，钟小妹. 基于事件逻辑的无线Mesh网络认证协议安全性证明[J]. 计算机工程与科学, 2017, 39(12): 2236-2244.
[12]	肖美华1，梅映天1,2，李伟1，李娅楠1，钟小妹1，宋子繁1. 基于时间戳私钥签名技术的Nayak-T协议安全性分析[J]. 计算机工程与科学, 2017, 39(12): 2252-2259.
[13]	袁红娟1,2,马艳芳3,潘海玉1,2. 模糊交互时态逻辑的模型检测[J]. 计算机工程与科学, 2017, 39(12): 2290-2296.
[14]	范林军1，史湘宁2，凌云翔1,3. 时钟有限自动机模型及其演化算法[J]. 计算机工程与科学, 2017, 39(02): 378-384.
[15]	吴格格，庄雷，张坤丽，王国卿. 移动支付协议PCMS的形式化分析和验证[J]. 计算机工程与科学, 2017, 39(01): 67-73.

一种自动化模型检测ANSIC程序的实用方法

A Practical Method for Automatically Model Checking the ANSIC Programs

PDF

可视化

摘要/Abstract

引用本文

使用本文

相关文章 15

编辑推荐

Metrics

本文评价