随着信息技术的飞速发展，各种软硬件系统已经渗透进了社会生产、生活的各个环节，这些系统正在深刻的影响和改变着整个人类社会的运作方式。人类社会的发展对各种计算机及软件系统的依赖程度越来越高。然而，软硬件系统的正确性与可靠性使得人们在享受信息技术带来的效率与便捷的同时，也面临着系统失效带来的风险。各种系统的集成与融合以及并发系统的大量出现使得软件的规模与复杂程度呈现出指数增长的趋势。因此，复杂软硬件系统的正确性与可靠性验证已经成为一个极具挑战的重要课题。模型检测作为一种形式化验证方法，能够严格地构建大规模系统模型并对其进行自动推理和验证。目前模型检测技术的研究热点已经从硬件验证转移到软件验证。状态空间爆炸问题、尤其是无限数据结构与控制结构导致的无限状态空间，是软件模型检测面临的最大挑战。随着各种软件系统的智能化程度越来越高，如何精确地构建智能推理系统模型也已经逐渐成为系统建模面临的新问题。此外，如何高效地对大规模反例进行自动理解，已经成为影响模型检测在软件验证中应用、普及的新障碍。因此，对模型检测理论及其在软件领域的应用进行深入研究具有较高的理论和应用价值。针对模型检测在验证复杂软件系统中面临的主要挑战，本文开展了以下几个方面的工作。1）提出了一种利用不动点计算对知识库进行建模的方法。该方法在给出条件迁移系统状态集构造函数的基础上，以Knaster-Tarski定理为理论依据对CTS构造函数的不动点及最小不动点的存在性进行了证明，进而证明了CTS状态集合S就是其构造函数的最小不动点。并在此基础上给出了CTS状态集的最小不动点计算求解方法，把模型构建过程转换为求解状态集合构造函数最小不动点的过程。该方法有效地提高了知识库的建模和错误诊断效率。2）提出了一种基于懒惰切片的状态空间搜索方法。该方法在发现伪反例时，把伪反例可行前辍的可行等价后继状态作为初始状态，并在截断状态引导下仅细化未被搜索过的局部状态空间，覆盖关系使该方法能够利用进入细化迭代前已经完成的工作证明给定性质的正确性，有效避免了基于CEGAR的切片方法导致的重复计算；懒惰切片产生的精度递增的反例路径也使得伪反例的判定可以通过仅具体化反例路径上最后一个路径片段完成，从而缩减了具体化该路径片段之前的所有路径片段的计算量；此外，通过仅保留事件守护条件中和当前过近似切片精度相关的条件，懒惰切片能够构造一个更加精确的过近似切片模型用于状态空间搜索。3）提出了两个懒惰切片的扩展算法。首先提出了基于懒惰切片的LTL模型检测算法，该方法通过对原始模型的过近似切片与给定性质的否定非确定性Büchi自动机求积，然后在乘积自动机上展开懒惰搜索使懒惰切片具备了验证LTL性质的能力，同时也提高了基本LTL模型检测算法对状态空间的压缩能力。此外，为了使懒惰切片算法具备处理无限状态空间模型的能力，提出了一种基于懒惰切片和抽象的正交化缩减方法，该方法通过把懒惰切片应用于抽象后得到的有限状态模型上，使懒惰切片能够借助抽象方法处理无限状态空间模型，同时进一步提高了模型检测器能够处理的状态空间规模。4）提出了一种基于克雷格插值的反例理解方法。该方法首先从模型检测器给出的反例失效状态开始，通过事件、及指派表达式推导规则计算出反例的最弱前置条件，然后使用SAT求解机给出反例最弱前置条件与初始状态的不一致证明，最后在该不一致性证明中解析出克雷格插值作为反例失效的原因，该计算过程能够在线性时间内完成，显著提高了反例理解的效率。