模型检测

*全面介绍模型检测原理与与实践方法。
*对模型检测领域的核心问题进行了清晰的阐述。 

模型检测是一种用于自动验证有限状态并发系统的技术，与基于模拟、测试和演绎推理的传统技术相比，具有许多方面的优势。本书共分18章，涵盖的主要内容包括模型检测的基本知识、模态逻辑、符号化技术、SATSolver、限界模型检测、自动机上的模型检测、抽象解释、程序分析、实时系统验证，同时介绍NuSMV和UPPAAL两个流行的模型检测器。

Edmund M.Clarke教授，美国卡内基 ? 梅隆大学计算机科学系教授，并且是ACM和IEEE会士。他在软硬件验证、自动定理证明、形式方法等方面享有崇高的国际声誉，2007年获得ACM图灵奖。
吴尽昭，广西大学副校长，长期从事高效能高可信计算与推理理论与工具的研究和开发，研究领域涉及符号计算、自动推理、形式化方法及其交叉、融合与应用；在国内外学术刊物和国际会议论文集上发表研究论文107篇，出版专著3部，获得软件著作权6项，申请专利3项；近年来承担国家自然科学基金、863、973子课题等国家、省部级科研项目10余项。

目 录
第1章 绪论 1
1.1 形式化方法的需求 1
1.2 硬件与软件验证 1
1.3 模型检测的流程 3
1.4 时序逻辑与模型检测 3
1.5 符号算法 4
1.6 偏序约简 6
1.7 缓解状态爆炸问题的其他方法 7
第2章 系统建模 8
2.1 并发系统建模 8
2.2 并发系统 11
2.3 程序翻译的实例 16
第3章 时序逻辑 18
3.1 计算树逻辑CTL* 18
3.2 CTL和LTL逻辑 20
3.3 公正性 22
第4章 模型检测 24
4.1 CTL模型检测 24
4.2 基于tableau结构的LTL模型检测 29
4.3 CTL*模型检测 33
第5章 二叉判定图 36
5.1 布尔公式的表示方法 36
5.2 Kripke结构的表示方法 40
第6章 符号模型检测 42
6.1 不动点表示 42
6.2 CTL符号模型检测 45
6.3 符号模型检测中的公正性 48
6.4 反例和诊断信息 50
6.5 一个ALU的例子 52
6.6 关系积的计算 54
6.7 符号化的LTL模型检测 61
第7章 基于? 演算的模型检测 68
7.1 简介 68
7.2 命题? 演算 68
7.3 求不动点公式的值 71
7.4 用OBDD表示? 演算公式 74
7.5 将CTL公式转化为? 演算 75
7.6 复杂度问题 76
第8章 实践中的模型检测 77
8.1 SMV模型检测器 77
8.2 一个实际的例子 80
第9章 模型检测和自动机理论 85
9.1 有限字与无限字上的自动机 85
9.2 使用自动机进行模型检测 86
9.3 检查Büchi自动机接受的语言是否为空 90
9.4 LTL公式转化为自动机 93
9.5 采用“On-the-Fly”技术的模型检测 97
9.6 检测语言包含的符号方法 98
第10章 偏序约简 100
10.1 异步系统中的并发 101
10.2 独立性与不可见性 102
10.3 LTL?X的偏序约简 104
10.4 一个例子 107
10.5 计算充足集(ample)集合 109
10.6 算法的正确性 114
10.7 SPIN系统中的偏序约简 117
第11章 结构间的等价性和拟序 122
11.1 等价和拟序算法 128
11.2 构建tableau结构 129
第12章 组合推理 133
12.1 多个结构的组合 134
12.2 判断假设保证证明方法的正确性 136
12.3 CPU控制器的验证 136
第13章 抽象 139
13.1 影响锥化简 139
13.2 数值抽象 141
第14章 对称性 154
14.1 群和对称性 154
14.2 商模型 156
14.3 对称性和模型检测 159
14.4 复杂度问题 160
14.5 实验结果 164
第15章 有限状态系统的无限簇 166
15.1 无限簇上的时序逻辑 166
15.2 不变量 167
15.3 再次分析Futurebus 169
15.4 图和网络文法 171
15.5 令牌环簇的不确定性结果 179
第16章 离散实时系统和定量时序分析 183
16.1 实时系统和单调变化率调度 183
16.2 实时系统的模型检测 184
16.3 RTCTL模型检测 185
16.4 量化时序的分析：小或延迟 185
16.5 飞行控制器 187
第17章 连续实时系统 192
17.1 时间约束自动机 192
17.2 并行组合 194
17.3 使用时间约束自动机进行建模 195
17.4 时钟域 198
17.5 时钟区 203
17.6 边界可区分矩阵 208
17.7 复杂度问题 211
第18章 结论 213
参考文献 215

序    言
目前，大家广泛认为有某种原因阻碍了实践“帮助计算机就会帮助人类更多”的理念，这使得我们更易于将复杂、敏感的系统丢给其他人去实现。这既不是机器的计算速度引起的，也不是计算能力造成的，而是工程师普遍缺乏设计并实现在所有环境中都会正确运行的复杂系统的自信。
这种设计有效性，即尽可能早地保证设计的正确性，是任何系统开发过程中都会遇到的挑战；而且关于这一问题的解决过程，在整个开发周期的成本和时间预算中所占的比例不断增加。
目前，保证设计有效性的方法依旧是持续了多年的模拟和测试技术。工程师已经在这两种技术领域积累了丰富的经验。在调试的早期阶段，这两种技术非常有效，但是经过它们检测后，系统设计仍然可能包含大量错误。随着系统设计越来越精确，这两种方法的工作效率急剧降低，每发现一个小错误都需要花费大量时间。此外，这两种方法还会导致一系列的问题：没有人知道这种技术的查错极限，更没有人能预测出经检测后设计中还剩余多少错误。随着设计复杂度的急剧增加，比如从大约五十万门的芯片设计提高到五百万门的芯片设计，一些有远见的项目经理已经预见到这些传统方法将要崩溃，并且它们将无力再扩展或提升。
形式化验证技术是一个非常具有吸引力的验证方法，可以用于替代模拟与测试，这种方法是本书的主旨。模拟与测试能够检测系统的部分可能行为与情况，但是不能确定系统是否还含有致命错误，而形式化验证却能对系统的全部行为进行彻底的检测。因此当系统设计被形式化验证方法证明为正确时，就蕴含了所有的行为已被检测通过，并且再也不用考虑是否达到足够的覆盖率或者是否含有行为缺失这样的问题。
这些年已经提出了多种形式化验证技术。本书集中介绍的模型检测方法，通过对给定反应系统(模型)中所有可达状态与行为进行(显式的或隐式的)彻底的检测，来验证系统规约的行为特性。
与其他方法相比较，模型检测方法有两个显著的优势：
?  自动进行，并且不要求使用者具有专业的数学知识(如定理证明)和经验。对于任何具有模拟检测经验的人，完全能够使用模型检测进行验证。同当前的验证方法相比，模型检测可以被视为一个更高级的模拟工具。
?  如果模型检测得出设计未能满足某些期望的性质，那么将产生一个反例来说明系统违反性质的具体行为。这种缺陷轨迹有助于理解检测失败的真实原因，同时也提供了修复此问题的重要线索。
这两个重要的优势，再加上可以对天文数字般的状态进行彻底的隐式枚举的符号模型检测方法，引起了形式化验证领域的根本变革，将模型检测技术从一个纯理论的学科转变为实际可行的技术。模型检测技术可以融入许多工业开发流程中，已经成为一种确保设计有效性的有价值的方法。
工业界普遍认同模型检测具有巨大的实力和潜力，大量的研究人员也在致力于模型检测技术的开发，所开发的产品已经应用于大型先进半导体电路和处理器公司的研发过程中。
非常幸运能够出现这本关于模型检测的原理与方法的权威性著作，这本书的作者从模型检测思想着手，全面介绍了模型检测中各种令人惊讶的技术，并终构建出一个成功的技术体系。
我对这本出色的参考书非常有信心。这本书将有助于读者(包括学生与从业人员)理解形式化验证特别是模型检测技术的原理与实现。

Amir Pnueli    
 
前    言
计算机科学中的多个领域都涉及有限状态并发系统，特别是数字电路与通信协议与这种系统关系紧密。这些系统研发过程中出现的逻辑错误对于电路设计者和程序员而言，都是一个非常棘手的问题，可能会推迟新产品的上市时间，也可能导致一些投入使用的重要设备发生故障。目前广泛使用的验证技术是测试和模拟，但当电路或协议的状态规模巨大时，这些技术无疑会遗漏重要的错误。虽然定理证明器、项重写系统和证明检测器都经过了长期和大量的研究，但是这些技术不但耗时，还常常需要许多人工干预。在20世纪80年代，一个被称为时序逻辑模型检测的验证技术由美国的Clarke与Emerson[61]以及法国的Quielle与Sifakis[219]分别独立提出。这种方法使用命题时序逻辑来表示性质规约，电路与协议被建模为状态变迁系统，并且提出一个用于确定规约是否在变迁系统上为真的高效查找过程，即检测变迁系统是否是性质规约的模型。
同机械化的定理证明或证明检测相比，模型检测在验证电路与通信协议方面有着多个重要的优势，其中重要的优势是检测过程的全自动化，使用者只需提供被检测的模型与性质规约的高阶描述。模型检测算法要么以结果为真终止，此时模型满足规约；要么给出一个反例指出性质违反规约的原因。在复杂变迁系统中，这种反例非常有益于发现和修正细微错误。模型检测过程相当快，通常大约几秒钟产生一个结果。在检测过程中，由于可以部分地检测规约，所以在获得有用信息之前不必构建完整的系统模型。当性质规约不能满足时，可以通过精心构建与当前规约不同的公式，来检测并定位错误的源头。除此之外，描述性质规约的逻辑能直接表示许多并发系统推理所需的性质。
模型检测的主要缺点是状态爆炸，这种情况发生在由许多系统组件并发演化构成的系统中。在这种情况下，整个系统状态的数目将按组件数量呈指数级增长。由于这个问题，许多形式验证的研究者预言模型检测对于大型系统是不实用的。但是，在20世纪80年代后期，模型检测技术所能检测的变迁系统的规模显著地增大了。
这种增长归因于高效表示布尔函数的二叉判定图结构的应用，它不但简洁地表示了变迁系统，也提升了布尔运算的速度。符号模型检测方法对同步电路特别有用。在验证异步协议时，可通过偏序约简技术来减少状态空间的规模。偏序约简的基础是，不同顺序事件对应的计算无法被性质规约区分，可以认为是等价的，因此只需为等价类保留一个典型的计算，检测这种约简空间即可。
基于以上这些技术，以及稍后在本书中介绍的其他一些技术，现在模型检测已经作为一种实用的验证技术在工业界中得到了广泛使用。实际上，几家公司正开始把模型检测工具推向市场。
我们认为这本书既可作为模型检测的简介，也可作为研究者的参考。我们试图包含尽可能多的内容而使其完整，但是这个领域的研究进展如此之快，以至于勉强跟上令人兴奋的新研究成果都不可能。这本书的若干部分与其他部分相比更加专业，在次阅读时可以跳过它们，这些部分在书中已经标出，它们主要针对从业者与研究者。我们真诚地希望这本书能够激励读者在模型检测领域做出更好的研究。
后，作者要感谢那些帮助创作这本书的人。首先想要对David Long表示我们的谢意，他的努力使这本书顺利出版。我们也想要感谢那些审阅初稿的人们，他们是：Eric Allen、Ilan Beer、Armin Biere、Sergey Berezin、Sergio Campos、Ching-Tsun Chou、Allen Emerson、Kousha Etessami、Nissim Francez、Masahiro Fujita、Yair Harel、Wolfgang Heinle、Hiromi Hiraishi、Neil Immerman、Somesh Jha、Irit Katriel、Shmuel Katz、Bob Kurshan、Kim G. Larsen、Yuan Lu、Jan Maluszynski、Will Marrero、Marius Minea、Bud Mishra、Ulf Nilsson、Wojciech Penczek、Amir Pnueli、Toshio Sekiguchi、Subash Shankar、Zeev Shtadler、Prasad Sistla、Frank Stomp、Wolfgang Thomas、Moshe Vardi、Dong Wang、Pierre Wolper、Bwolen Yang、Husnu Yenigün、Yunshan Zhu。如果我们遗漏了对这本书有所帮助的人们，我们在此道歉。Edmund Clarke感谢Michael Shostak在写书的过程中所给予的鼓励。Doron Peled感谢Marta Habermann于1998年在CMU的春季学期中提供了一个舒适安逸的居所。