随着计算机软硬件系统日益复杂，如何保证其正确性和可靠性已经成为日益紧迫的问题。对于并发系统，由于其内在的非确定性，这个问题难度更大。在过去的几十年间，各国研究人员为解决这个问题付出了巨大的努力，取得了重要的进展。在为此提出的诸多理论和方法中，模型检测以其简洁明了和自动化程度高而引人注目。 模型检测的研究始于上世纪八十年代初，当时Clarke，Emerson等人提出了用于描述并发系统性质的CTL逻辑，设计了检测有穷状态系统是否满足给定CTL公式的算法，并实现了一个原型系统。这一工作为对并发系统的性质的自动化验证开辟了一条新的路径，成为近二十五年来计算机科学基础研究的一个热点。随后不久出现的符号模型检测技术使这一方法向实际应用性迈出了关键的一步。模型检测已被应用于计算机硬件、通信协议、控制系统、安全认证协议等方面的分析与验证中，取得了令人瞩目的成功，并从学术界辐射到了产业界。许多公司，如Intel、HP、Phillips等成立了专门的小组负责将模型检测技术应用于生产过程中。 模型检测的基本思想是用状态转换系统M表示系统的行为，用时态逻辑公式φ描述系统的性质。这样“系统是否具有所期望的性质”就转化为数学问题“状态转换系统M是否是公式φ的一个模型?”，用公式表示为M |=φ?。对有穷状态系统，这个问题是可判定的，即可以用计算机程序在有限时间内自动验证。 模型检测的研究大致涵盖以下内容：时态逻辑、模型检测算法及其时空效率(特别是空间效率)的改进以及支撑工具的研制。这几个方面之间有着密切的联系。不同时态逻辑的模型检测算法的复杂性不一样，优化算法往往针对某些特定类型的逻辑公式。 模型检测基于对系统状态空间的穷举搜索。对于并发系统，其状态的数目往往随着并发分量的增加呈指数增长，因此当一个系统的并发分量较多时，直接对其状态空间进行搜索在实际上是不可行的。这就是所谓的状态空间爆炸问题。状态空间爆炸问题是有效应用模型检测方法的主要困难所在，为此研究人员提出了许多方法来克服状态空间爆炸问题，包括基于二叉图的符号化模型检测技术，抽象，组合验证，偏序归约，对称归约。但是每一种方法都有其特有的使用场景，到目前为止不存在一个通用的方法。 1999年，奥地利学者Armin Biere提出了一种新的克服状态空间爆炸问题的符号化技术一基于命题公式可满足性判定的有界模型检测技术。其主要思想是在系统的有限运行空间上检测属性是否失效，并把属性的失效归约到命题公式的可满足性判定上。基于DPLL算法的命题公式可满足性判定过程中不存在基于二叉图的方法中状态快速增长的问题。命题公式可满足性判定工具可以处理具有几千个变量的命题公式。这两点保证了有界模型检测技术的有效性。 自Armin Biere提出有界模型检测的技术以后，其验证思想得到了广泛的认可和重视，许多研究工作围绕着提高有界模型检测的效率和扩展其验证领域展开。本篇论文系统的研究了基于有界模型检测思想的符号化技术，主要工作是(1)提高有界模型检测的执行效率，包括减少内存需求，降低运行时间；(2)扩展有界模型检测技术的验证领域； (3)运用有界检测的思想验证更多的属性。具体的讲我们的工作包括以下几个方面： ·提高有界模型检测的效率，减少其内存需求 —在有界模型检测中对于某些验证的属性，我们发现存在等价的有限路径。有界模型检测通过搜索所有的有限路径来检测属性的失效，这样对于等价的路径存在重复搜索，从而降低了可满足性判定的效率。我们在线性时态逻辑的有界模型检测中引入了偏序规约技术。偏序规约的引入使得对于LTL—x属性SAT工具可以避免等价路径的重复搜索。对于选定的验证实例，我们的实验数据表明在引入偏序规约技术以后运行时间至少可以降低50％。另外，我们在分支时态逻辑ACTL的有界模型检测中，增加了对路径的约束，使得等价的路径同样避免了重复搜索。 — 有界模型检测技术对于异步系统不是特别的有效，因为异步系统的转换关系表现为局部构件转换关系的析取。这种析取表示导致最后得到的命题公式过大，SAT工具无法承受。针对Petri网的特性，Shougo提出了一种新的转换关系编码方法，他们的方法仅仅对1界Petri网的可达性、L0、L1活性检查是合适的。我们对Shougo的方法进行了改进，使之可以有效的验证LTL—x属性，同时将验证模型扩展到n界Petri网上。— 在Petri网的有界模型检测中，对于每一个可达状态认为每个变迁都有引发的可能，这将导致最后得到的命题公式过大。事实上，在每一个可达状态下仅有少数变迁可以引发。为此，我们提出了一个算法来估算k步可达的状态下可以引发的变迁。算法的时间复杂性对于Petri网的大小和输入的步长是多项式的。因此该算法可以显著提高有界模型检测的时空效率。 — 张文辉等提出了一种基于搜索空间划分的模型检测技术。对于特定的系统他们的方法可以有效的克服状态空间爆炸问题，但是对于Petri网其划分策略是无效的。我们利用搜索空间划分的思想，对于具有对称结构的Petri网提出了一个划分策略。对于选定的验证实例，实验数据表明我们的方法至少可以减少60％的内存需求。 ·扩展有界模型检测技术的验证领域 — 模型检测多智体系统是目前的研究热点，状态空间爆炸依旧是验证的困难所在。许多学者提出运用有界模型检测的思想来克服状态空间爆炸，因此出现了很多组合了时态逻辑和知识逻辑的属性规约语言及其有界模型检测算法。我们提出了一种新的属性规约语言，同时给出了该属性的有界模型检测算法。和存在的工作相比我们的创新点主要在于：(1)属性规约语言融合了带有过去算子的线性时态逻辑和知识逻辑。过去算子的引入可以使我们非常紧凑的自然的描述系统的属性，而属性的紧凑性对于最后得到的命题公式的大小是非常重要的。(2)存在的工作都没有讨论多智体的有界模型检测中非常重要的完全界问题。对于我们的属性规约语言，给出了其完全界。 — 对于基于消息传递的并发软件，针对其并发特性我们提出了一种基于事件和状态的属性规约语言。该语言集成了时态逻辑，事件和状态，使得我们可以非常简洁的自然的表示验证的属性。同时我们提出了一种基于反例寻找的验证框架，该框架的最大特点是融合了基于命题公式满足性判定的有界模型检测，抽象和组合验证的思想。三种状态空间约简方法的融合有效的克服了状态爆炸问题。同时在该规约语言的界模型检测中，我们引入了偏序规约的技术，使得等价的有限路径避免了重复搜索，减少了运行时间。 ·运用有界检测的思想验证更多的属性 — 到目前为止有界模型检测只是被用来检测全称属性，对于更广泛的属性目前还没有任何相关的研究。有界模型检测的思想是在有限的运行空间上判定全称属性的失效性。事实上对于一些更广泛的属性并不需要在全局的运行空间上判定其有效性，在有限的运行空间上也可以判定。 对于计算树时态逻辑CTL，我们应用有界模型检测的思想，提出了一个新的基于QBF的符号化模型检测技术。我们的基本思想是在有限的运行空间上定义CTL的有效性，并将有效性的检测归约到QBF公式的满足性的判定上，使得QBF公式是可满足的当切仅当CTL公式在有限运行空间上是有效的。我们的方法是可靠的，即CTL在有限运行空间上的有效性是对其在在无穷空间上有效性的逼近。同时我们的方法是完全的，即CTL在无穷运行空间上是有效的，一定存在一个有限运行空间使得CTL在该有限空间上是有效的。 基于命题公式满足性判定的有界模型检测算法的成功很大程度上归功于基于DPLL的满足性判定算法在判定满足性的过程中不会出现空间的快速增长。同理基于DPLL的QBF算法在检查满足性的判定过程中也不会出现空间的快速增长。另外，已经存在QBF工具能够处理具有上千个变量的QBF公式。这两点保证了基于QBF方法的有效性。