电脑的使用越来越普及,人们对电脑的依赖也越来越严重。电脑硬件由于发展时间较长,硬件的协议比较简单,其检测手段丰富、成熟,安全性要比电脑软件的安全性高一个等级,甚至更多。同时,生活信息化加深了人们对软件的依赖,软件的质量的好坏,给使用软件的各行各业有很深的影响,因此人们对软件质量推出了越了越高的要求。在软件开发的软件过程思想出现以后,如何提高软件质量一直是计算机界研究的重点。传统的软件测试,使用针对性的测试,可以指出软件存在的特定缺陷,但是由于测试并不能够无穷的进行,所有此方法不能指出所有的错误,同时也不能证明软件的正确性。形式化方法使用数学方法,能较好的证明系统的完整性、正确性、安全性。形式化方法中的模型检验以其高效、自动化使其成为研究的热点。自模型检验技术提出以来,人们将其应用到硬件驱动和协议的开发上,随着应用过程中的出现问题、解决问题的过程,不断有相关的技术、理论提出。符号化方法使模型检验在检验时,能够检验10¹²⁰个状态,这使模型检验技术完全胜任了硬件驱动和协约验证的验证问题。在模型检验在硬件、协议验证上获得巨大的成功后,人们将模型检验的应用对象的研究重点放到软件系统上来。使用模型检验到软件系统的的步骤大概分为:对待检验系统进行建模、用模型性质描述语言对程序性质进行描述、使用模型检验工具检验模型是否满足性质。对模型检验的研究基本集中在这三个步骤:1)怎样增加模型检验能够解决问题的范围;2)更方便、灵活的描述程序性质,3)提高模型检验过程的效率。而状态爆炸问题是模型检验工具在软件系统中使用的瓶颈。本文提出一种基于模型检验的软件分析方法。本方法结合软件的信息流分析技术,使用CTL描述语言和NuSMV模型检验工具。该方法能够确定给定C/C++源程序是否满足我们预先已定义的程序性质。这些性质包括:1)不存在未初始化变量;2)内存分配和释放配对;3)不存在变量未使用;4)不存在野指针。通过使用NuSMV模型检验工具,结合模型检验和程序分析技术,完成对程序相关性质的分析。本文的主要工作包括以下几个部分:1.将信息流分析中的控制流程图的等价Kripke结构作为模型检验模型,简化了对软件进行模型检验时建模的工作。2.对抽象语法树、控制流程图概念进行扩展,并制定规则将控制流程图转换为等价Kripke结构,最后证明转换后的模型与源代码的等价性。3.制定了将模型和CTL公式描述的性质转换为模型检验工具NuSMV的输入的转换规则。