复杂的软件系统往往有很多未知的系统错误，这些潜在错误给软件的可靠性、稳定性带来了很大的挑战性。模型检测技术(建模)能够从软件的源代码中提取出该软件的形式化模型，继而可以采用验证工具对该形式化模型进行验证并且能够定位出软件的潜在错误。然而，事实证明，人工建模是非常耗时耗力并且建模很容易引入未知错误，不能如实反映软件系统。对于大规模的软件系统来说，即使是经验丰富的专家也觉得难以下手。因此，人们越来越希望有一种自动或者接近自动的模型提取方法。 基于以上分析，本文对建立软件的形式模型进行了大量的研究，并且提出了一种解决方案——自动提取源代码的验证模型(形式模型)。本文的研究工作包括：1、对C语言的各种语句进行语义分析，把分析的语句等价转换成以表达式的形式来描述，从而建立了形式模型；2、在实现过程中，本文选用了一种C语言的解释工具——CTool，把源代码转换成抽象语法树(AST)，从而实现对语句抽象等级模型的建立。然后对抽象语法树进行等价语义转换，从而建立表达式抽象等级模型，也就是形式模型。 本文利用Cadence SMV工具对形式模型进行模拟实验，计算模型的结果。比较C源代码的结果和模型的计算结果，两者是相等的。实验结果表明提取的模型和源代码是等价的，从而证明本文提出的模型自动提取方法是有效的。本文提出的自动模型提取方法节省了建模的耗费，同时也真实的反映系统的源代码。