在软件的开发过程中,需求和程序分别是头尾两个阶段的软件形态。人们最终的目的就是要将需求转换为程序。在现今技术条件下,这一转换过程中人的技术能力仍然是软件质量的主导因素。虽然自动化工具已经逐渐被广泛应用,比如需求建模和模型检测、模型转换、自动化测试、以及少数几个领域中的程序自动生成技术等等,但是在软件开发阶段,手工编码在绝大多数领域仍然是主要的开发手段。那么,保证手工生产出来的程序符合之前经过验证的需求成为这一阶段的关键问题。此外,在许多软件开发项目中,需求模型与程序源代码脱节,花费了大量人力和财力所得到的需求模型在软件开发后期只具备主观参考价值,甚至被作为摆设,而不能发挥应有的作用,造成了软件开发中开支的浪费。目前要判断程序是否符合需求需要对程序进行仔细而充分的测试,但测试的效果也存在多个因素的制约,例如人的主观判定问题、测试的覆盖率问题、需求和程序更新后测试用例的演化问题等。针对上述问题,本文提出一个新的方法,就是将程序和已经建立好的需求模型进行自动化比较检测,从中寻找差异,帮助人们对可能存在的问题进行分析。这项工作包含以下三个方面的研究：1、在标记迁移系统的基础上扩展出并发状态机模型。该模型适合同时对需求和程序进行描述,且方便从需求和程序进行转换。并且以标记迁移系统为基础,通过对迁移进行扩展支持对并发的描述。其表达能力强,结构简单,适合进行模型比较。2、提出对C语言程序进行程序分析、提取完整的并发状态机模型并进行抽象的完整方法。其中采用新提出的基于域传播的别名分析法对C语言进行函数指针分析,解析每一个间接调用,从而得到完整的程序流图；需求模型和程序模型的数据对应配合数据流分析,使得用户通过少量的人工干预就可以得到需求和程序之间的元素对应关系；并发的识别能够对并发API进行特殊处理,将其转换为抽象并发描述,并将程序的流图转换为并发状态机模型。3、研究模型比较检测的理论,并提出检测的方法和技术。理论部分的研究包括从需求到程序的模型演化研究,为模型比较检测方法的正确性提供理论依据,也为检测的内容提供理论基础。按照模型比较检测的方法和技术建立功能完整的检测工具,使之能够对需求和程序进行比较和定位差异,协助软件测试和维护人员对程序源代码进行分析。此外,本文对所提出的模型比较检测方法在其他模型上的应用进行了理论研究,为模型比较检测方法支持对其它模型进行检测提供理论依据。