形式化验证是安全软件设计和实现的重要保障之一。在各种形式化验证方法中，模型检测以其自动化程度高且能提供反例来帮助纠错等优点而得到应用和推广。但是，在对大型软件进行模型检测时，经常因为出现状态空间爆炸，而使检测难以完成。本文对状态空间爆炸问题进行了研究和分析，并对线性时序逻辑LTL(Linear Temporal Logic)模型检测过程做出了改进。主要包括：　　 (1)研究分析了模型检测过程以及目前解决状态空间爆炸的方法。总结和分析了模型检测的机制和原理；从检测原理和过程中研究状态空间爆炸的原因。总结、比较了目前解决状态空间爆炸问题的主要方法。并根据状态空间爆炸的原因对目前的解决方法进行分类，通过分析和比较，总结了这些方法的优缺点。　　 (2)研究分析了程序切片的过程和方法。讨论了条件切片、动态切片和静态切片等方法的原理，并对它们的作用和效果进行了分析和对比。研究和分析了后向切片和前向切片等两种程序切片方式。通过对它们的分析和总结，为本文提出的对模型检测过程的改进方法奠定了基础。　　 (3)提出了一种基于后向静态切片的模型检测改进方法，在模型检测过程中加入后向静态切片。并根据待检测需求属性的不同类别，分别定义了不同的切片准则构造方法。对切片后和切片前程序对待检测属性是否具有同样的满足性进行了分析，给出了切片后满足性可保持的属性和不可保持的属性，并给予了证明。　　 (4)在前文所提的改进的基础上又提出在模型检测过程中加入LTL属性分解的改进。通过对LTL属性的研究，定义了LTL属性的可分解性，给出了LTL属性的分解方法。并对改进方法的正确性给予了证明。　　 (5)基于改进的模型检测方法，设计并实现了一个切片和属性分解模型检测系统，并通过实验验证了改进的效果。在Linux平台上设计实现了基于改进方法的检测系统，并选取较有代表性的实例对其进行检测，验证和说明改进的效果。