一种自动化模型检测ANSI-C程序的实用方法
首发时间:2009-05-01
摘要:模型检测是一种验证有穷状态系统时序逻辑属性的形式化方法。为了利用模型检测技术来测试一个系统,通常的办法是手工构建一个抽象模型。然而这个方法有诸多不足,如成本过高,易引入建模错误等。本文提出了一种自动化模型检测ANSI-C程序的方法,并开发了C2Spin,它能够自动分析ANSI-C源代码,并生成PROMELA验证模型。配合SPIN,C2Spin可以自动检测软件中的错误,比如死锁等。在初步实验中,C2Spin发现了SPIN4.3.0的一处语义错误,以及Holzmann对两个经典互斥算法的实现中的活锁隐患,这些结果表明使用C2Spin检测软件错误是可行的。
关键词: 模型检测 程序验证 ANSI-C SPIN PROMELA
For information in English, please click here
A Practical Method for Automatic Model Checking ANSI-C Programs
Abstract:Model checking is a formal method for verifying the temporal logic property of finite state system. An abstract model is usually created by hand, but this approach has a few weaknesses, such as high cost and man-made model mistake. This paper presents a practical method for model checking ANSI-C programs automatically. We built C2Spin, a system that analyze the C source code and extract PROMELA verification model from the source code directly. Then the SPIN model checker can determine whether a program satisfies a property, like deadlock. In preliminary experiments, C2Spin found a semantic bug in SPIN4.3.0 and livelocks in the Holzmann’s implementation of two classic mutual exclusion algorithms. The results show that it is feasible to detect software errors using C2Spin.
Keywords: Model Checking Program Verification ANSI-C SPIN PROMELA
论文图表:
引用
No.3189046612612411****
同行评议
勘误表
一种自动化模型检测ANSI-C程序的实用方法
评论
全部评论0/1000