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

A Practical Method for Automatically Model Checking the ANSI-C Programs

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

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 cheeking 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 sig- nificantly. 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.