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

摘要：

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

关键词：形式化方法、模型检测、模型提取、ANSI-C、PROMELA

所属期刊栏目：32

分类号：TP301.2(计算技术、计算机技术)

资助基金：国家自然科学基金资助项目60673155;国家"可信软件"重大研究计划资助项目90718008

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

页数：共4页

页码：79-82