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

关键词：形式化方法 模型检测 模型提取 promela 

单位：