信息技术在现代生产生活各方面的应用越来越广泛,作为信息技术核心支撑的软件系统也变得越来越重要,其应用正在逐步渗透到社会的各个领域中去。时至今日,现在各行各业中的应用已经很难离开软件而独立运作了。软件系统已经成为了与我们的工作、生活密不可分的重要部分。软件系统的可靠与否,直接影响着人们的生产生活。在这个背景下,人们对软件系统的可靠性提出了越来越高的要求。软件系统中最重要的实体形式是源代码,软件系统的可靠性需要源代码的可靠来保证。伴随这软件规模的增长,软件开发的周期越来越长,如何保证源代码的正确性一直是计算机学界研究的重点和热点问题。模型检测技术是一种常见的形式化方法,该方法最初用于硬件设计验证和协议分析。伴随着各种软件问题的出现,研究者提出用模型检测技术验证软件巾的相关特征或性质是否满足系统需求或设计要求,这一技术近年来已经被用于针对软件源程序级的验证。本文提出了一种基于模型检测技术的源代码级的验证方法。本方法通过对源代码的抽象语法信息的分析以及与SPIN模型检测工具输入语言Promela的比较,给出了一种从C语言源代码到Promela语言的转换方法。通过这种转换,我们可以得到与C源代码一致的Promela模型,从而可以借助SPIN模型检测工具来间接地验证C语言源代码中的相关性质。本文所做的主要工作包括如下几个部分：首先,通过对源代码的抽象语法信息的分析,得到与源代码对应的控制流图结构,该控制流图结构作为下一步转换工作的基础；其次,对Promela语言和C语言抽象语法信息进行了比较分析,给出了包括控制结构、函数和指针在内的相应转换规则；最后,在上述转换规则的基础上,实现了一个原型工具,能够完成从CFG到Promela的转换,并且实现用SPIN进行指定性质的验证。