论文摘要
随着信息科学技术的迅猛发展,软件被广泛应用在现代社会的各个领域,如何确保软件的安全可靠已经成为计算机科学领域共同关注的一个焦点问题。采用形式化方法对系统进行分析和验证,是构造可靠软件的一个重要途径,模型检测就是这些形式化方法中的一种。模型检测可以形式化地验证有限状态并发系统的正确性,该方法具有很多的优点,包括自动化程度高、速度较快、在属性不满足的时候能够给出反例路径等。然而,该方法的一个比较突出的缺陷是“状态空间爆炸问题”。目前,研究如何自动有效地对待检测系统模型进行简化,使得软件的模型检测过程顺利完成,已经成为该研究领域的一个重要研究课题。本文立足于待检测线性时序逻辑（LTL）属性分解方法的研究,对模型检测中状态空间爆炸问题的缓解技术进行分析和实现：（1）阐述和总结了模型检测中的基本理论和技术要点,包括其相关概念、主要过程、LTL和CTL属性检测算法、典型的模型检测工具及其应用场合。在此基础上,指出模型检测技术的瓶颈问题,即“状态空间爆炸”,从不同层次上梳理和分析了导致该问题的主要因素,比较了目前解决该问题采用的方案。（2）介绍和分析了模型检测工具SPIN的理论基础,包括其主要特点、基本框架组成、基于Promela建模语言的建模方法,探究了SPIN中的核心算法并结合实例给出了SPIN的检测过程。此外,本文对SPIN中缓解状态空间爆炸问题的技术方案,如偏序规约,On-the-fly等,进行了研究和总结,为本文的主要工作垫定基础。（3）本文提出了一种基于LTL属性分解的切片模型检测方法。根据LTL属性中逻辑与时序操作符的常见组合情况,提出了LTL属性的可分解模式和不可分解模式,针对LTL属性进行分解,根据子属性构建的切片准则进行切片,从而将对原模型上原属性的检测转化成对复杂度较低的子模型上各个子属性的分别检测。该方法可以自动地进行,同时能与偏序规约等技术相结合,辅助完成模型检测过程,缓解状态空间爆炸。（4）基于所提出的方法,在模型抽取工具FeaVer和切片平台Frama-C之上,设计和实现了一个自动化的原型系统。选取一些待检测的实验对象,对它们状态空间的简化效果进行了分析和比较。实验结果表明,所提出的方法可以有效地缓解状态空间爆炸,使模型检测过程顺利完成。