软件模型检测是一种使用形式化方法验证软件可靠性的重要技术方法。根据采用方法逼近方向的不同,软件模型检测可以分为上逼近方法和下逼近方法。本文中所研究的抽象-精炼方法,是对上下逼近方法的融合,它涵盖了上逼近方法和下逼近方法并具有更好的性质。传统的软件模型检测根据所使用的程序状态模型的不同,分别使用上逼近和下逼近方法进行分析,因此与相应模型紧密耦合的算法也常具有较大区别。这种内在的区别使得软件模型检测算法之间难以复用,同时算法输出的结果间也难以相互使用。近年来,一些关于软件模型检测的上下逼近融合方法研究开始兴起,通过设计状态融合的操作运算,使得上下逼近方法的状态得以混合,在一定程度上做到了结果相互使用,但是这种使用依然是浅层的。不同范式的软件模型检测方法没有做到深入地融合,其根本原因在于缺少一个统一的对软件抽象状态进行描述的模型。现有的模型多是基于不同形式的逻辑建立的状态存储和推理系统,其本身是依附于具体状态之上,着重描述程序的分立状态,缺乏对程序整体结构信息的描述和分析。针对以上问题,本文的具体研究内容如下:（1）从软件模型检测中的下逼近方法入手,以有界模型检测作为切入点,分析了有界模型检测方法在处理一般输入程序时所遇到的困难。这种困难存在于状态空间的表示和程序实际的执行流之间在距离上并不一致,导致在使用有界模型检测方法进行状态遍历时,其遍历的状态与目标状态集产生偏差,即发生了冗余的状态遍历,并最终导致方法实际性能的下降。针对这种问题,本文提出了一种度量程序执行流的方法,其度量出的距离可以指导状态遍历的方向,从而使得状态空间与执行流更加贴合,并通过实验验证了其对一般的程序片段的有效性。通过对下逼近方法的研究,在改进了有界模型检测方法的基础上,同时发现了一般程序的状态空间存在的两个基本方向属性:深度和广度。（2）针对在上逼近中应用较为广泛的谓词抽象在处理循环结构时容易落入循环中产生冗余遍历的问题,本文提出了基于K-归纳法对谓词抽象技术的上逼近方法的改进方法。这种方法可生成循环不变量,将谓词抽象从完整的检测循环中分离,成为具有一定模块化特征的子方法,并将K-归纳法从具体状态空间中提升到抽象状态空间。本文基于抽象-精炼方法的思想设计了K-归纳法和谓词抽象的组合方法。通过实验验证了该方法在处理循环程序片段中的有效性,且不会对其它类型程序造成显著的性能影响。通过对上逼近方法的研究,本文改进了谓词抽象方法对循环程序等的检测性能,并且发现该方法具有模块化和参数化的特性。（3）基于以上研究,本文继而着手对抽象-精炼类算法的统一结构进行研究。分析了一般抽象-精炼软件模型检测方法的公共性质,并在此基础上分别对下逼近方法和上逼近方法进行了解耦,建立了统一的模块化抽象-精炼方法的算法表示。该算法具有更为强大的灵活性以及普适性,使得传统的模型检测方法经模块化后成为该算法的子方法,并通过实验证明了该模块化方法不会对传统方法产生额外性能影响。（4）本文最后针对软件模型统一状态空间的表示和它所具有的性质开展了研究,建立了针对程序结构信息的状态模型,并提出了模型所具有的重要属性--对偶性。以之为基础,本文分析和建立了模型中的正交特性,并对抽象-精炼方法的高效性进行了解释。最后,利用该特性将模型映射到度量空间,推导了模型所具有的不确定特性,给模型检测方法的性能提供了边界参考。