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

• 作者: MIAO Li 张大方 王大伟
• 来源期刊: 计算机工程与科学
• 学科: 工学
• 关键词: 形式化方法 模型检测 模型提取 ANSI-C PROMELA
• 年，卷（期）: 2010,（4）
• 所属期刊栏目: 软件工程
• 页码范围: 79-82
• 页数: 4页
• 分类号: TP301.2
• 字数: 4219字
• 语种: 中文
• DOI: 10.3969/j.issn.1007-130X.2010.04.022

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张大方	湖南大学计算机与通信学院	295	2498	22.0	33.0
5	王大伟	湖南大学计算机与通信学院	2	4	1.0	2.0