电子工业出版社-网上书店

模型检测是一种用于自动验证有限状态并发系统的技术，与基于模拟、测试和演绎推理的传统技术相比，它具有许多方面的优势。本书共20章，涵盖的主要内容包括模型检测的基本知识、系统建模、时序逻辑、符号模型检测技术、SMV模型检测器、模型检测与自动机理论、偏序约简、抽象解释、有限状态系统的无限族、实时系统验证等。

目    录
第1章  第二版概述	1
第2章  第一版概述	2
2.1  形式化方法的需求	2
2.2  硬件与软件验证	2
2.3  模型检测的流程	4
2.4  时序逻辑与模型检测	4
2.5  符号算法	5
2.6  偏序约简	7
2.7  缓解状态空间爆炸问题的其他方法	7
第3章  系统建模	9
3.1  变迁系统和Kripke结构	10
3.2  非确定性和输入	11
3.3  一阶逻辑和符号表示法	11
3.4  布尔编码	14
3.5  数字电路建模	15
3.5.1  状态保持单元	15
3.5.2  同步电路	15
3.5.3  异步电路	16
3.6  程序建模	17
3.6.1  顺序进程	17
3.6.2  并发进程建模	19
3.7  公平性	23
本章文献注释	24
习题	24
第4章  时序逻辑	25
4.1  时序逻辑CTL*	25
4.2  CTL*的语法和语义	27
4.2.1  CTL*的语法	27
4.2.2  CTL*的语义	27
4.2.3  负范式(NNF)	29
4.3  基于CTL*的时序逻辑	29
4.3.1  分支时间逻辑CTL	30
4.3.2  全称计算树逻辑ACTL*和ACTL	31
4.3.3  线性时序逻辑LTL	32
4.3.4  各种CTL*子逻辑的关系	32
4.4  命题逻辑的集合型原子命题和集合语义	33
4.5  公正性	33
4.6  反例	34
4.7  安全性和活性	35
本章文献注释	36
习题	36
第5章  CTL模型检测	38
5.1  显式状态表示法的CTL模型检测	38
5.2  基于公正性约束的CTL模型检测	42
5.3  基于固定点计算的CTL模型检测	43
5.3.1  固定点理论	43
5.3.2  基于固定点的可达性分析	46
5.3.3  基于固定点的CTL模型检测算法	47
5.3.4  基于固定点的公正性	49
5.3.5  有限路径上的固定点特征	51
本章文献注释	51
习题	51
第6章  LTL和CTL*模型检测	52
6.1  构建语义表	52
6.2  基于语义表的LTL模型检测	55
6.3  构造语义表方法的正确性证明	56
6.4  CTL*模型检测	60
本章文献注释	62
习题	62
第7章  无限字上的自动机和LTL模型检测	63
7.1  有限字上的有限自动机	63
7.1.1  确定性和补自动机	64
7.2  无限字上的有限自动机	64
7.3  确定性和非确定性Büchi自动机	65
7.4  Büchi自动机的交自动机	66
7.5  空自动机检测	67
7.5.1  基于双DFS算法的空自动机检测	68
7.5.2  双DFS算法的正确性	69
7.6  广义Büchi自动机	70
7.7  自动机和Kripke结构	71
7.8  基于自动机的模型检测	72
7.9  LTL公式转化为自动机	73
7.10  LTL到自动机的高效转换	75
7.10.1  算法概述	75
7.10.2  数据结构	76
7.10.3  算法细节	77
7.11 采用即时技术的模型检测	80
本章文献注释	81
习题	82
第8章  二叉决策图和符号模型检测	83
8.1  布尔公式的表示	83
8.2  Kripke结构的OBDD	87
8.3  CTL符号模型检测	88
8.3.1  量化布尔公式	89
8.3.2  符号模型检测算法	90
8.4  符号模型检测中的公正性	91
8.5  反例和佐证	91
8.6  关系积的计算	94
8.6.1  分割的变迁关系	95
8.6.2  合并划分	99
本章文献注释	99
习题	100
第9章  命题满足性	101
9.1  合取范式	101
9.2  命题逻辑译为CNF的方法	102
9.3  基于二分搜索的命题满足性	103
9.3.1  递归的二分搜索	103
9.3.2  基于迹的二分搜索	105
9.4  布尔约束传播(BCP)	106
9.5  冲突驱动的子句学习	107
9.5.1  蕴含图	107
9.5.2  子句学习	108
9.5.3  基于CDCL的归结证明生成方法	109
9.6  启发式决策	109
本章文献注释	110
习题	111
第10章  基于满足性的模型检测	113
10.1  有界模型检测	113
10.1.1  有界模型检测总览	113
10.1.2  可达性	114
10.1.3  最终性	116
10.1.4  LTL的有界模型检测	117
10.1.5  完备性阈值	118
10.2  基于k归纳的可达性验证	119
10.2.1  基于命题SAT的归纳	119
10.2.2  泛化的k归纳	120
10.2.3  完备性	121
10.3  基于归纳不变式的模型检测	121
10.4  基于克雷格插值的模型检测	122
10.4.1  克雷格插值	122
10.4.2  面向归结证明的克雷格插值	123
10.4.3  基于克雷格插值的可达性检测	124
10.4.4  正确性	126
10.5  性质导向的可达性分析	126
10.5.1  概述	126
10.5.2  算法的主循环	127
10.5.3  extendFrontier算法	128
10.5.4  正确性	129
本章文献注释	129
习题	130
第11章  结构间的等价性和预序	131
11.1  互模拟等价	131
11.2  公正的互模拟等价	135
11.3  模型间的预序关系	135
11.4  互模拟和模拟关系的博弈	138
11.5  等价和预序算法	138
本章文献注释	139
习题	140
第12章  偏序约简	141
12.1  异步系统中的并发	142
12.2  无关性与隐匿性	143
12.3  LTL?X的偏序约简	145
12.4  实例分析	148
12.5  充足集的计算	150
12.5.1  条件检测方法的复杂度	150
12.5.2  计算充足集的启发式策略	151
12.6  算法的正确性	154
12.7  SPIN系统中的偏序约简	157
本章文献注释	161
第13章  抽象	162
13.1  存在性抽象	162
13.1.1  局部约简	165
13.1.2  数据抽象	166
13.1.3  谓词抽象	167
13.2  抽象模型的计算方法	168
13.2.1  软件程序的抽象	168
13.2.2  基于局部约简的同步电路抽象	170
13.3  反例引导抽象精化(CEGAR)	172
13.3.1  假反例	172
13.3.2  面向ACTL*的抽象精化框架	173
13.3.3  识别假反例	173
13.3.4  抽象模型的精化	176
本章文献注释	178
第14章  软件的模型检测	180
14.1  程序的控制流图表示方法	180
14.2  基于符号执行的断言检测方法	181
14.3  基于谓词抽象的程序验证	182
14.3.1  布尔程序	183
14.3.2  将普通程序惰性抽象到布尔程序的方法	184
14.4  完整实例	186
14.4.1  程序	186
14.4.2  性质规约	187
14.4.3  抽象程序	189
本章文献注释	191
第15章  基于自动学习的验证	192
15.1  Angluin的L*算法	192
15.1.1  实例分析	194
15.2  组合推理	195
15.3  面向通信组件的假设-保证型推理	196
15.3.1  系统模型	197
15.3.2  性质与满足性	198
15.3.3  LTS中假设-保证型范式的实现	199
15.3.4  基于学习的假设-保证机制	199
15.3.5  面向假设-保证规则的学习算法实例	201
15.4  黑盒检测	203
15.4.1  执行模型	203
15.4.2  简单解决方案	204
15.4.3  基于学习的算法	205
15.4.4  Vasilevskii-Chow算法	205
本章文献注释	206
第16章  面向μ演算的模型检测	208
16.1  概述	208
16.2  命题μ演算	208
16.3  求固定点公式的值	211
16.4  采用OBDD表示μ演算公式	214
16.5  将CTL公式转换到μ演算	216
本章文献注释	216
第17章  对称性	218
17.1  群和对称性	218
17.2  商模型	220
17.3  基于对称性的模型检测	222
17.4  复杂度问题	224
17.4.1  轨道问题和图同构	224
17.4.2  轨道关系和OBDD	226
17.5  实验结果	228
本章文献注释	229
第18章  有限状态系统的无限族	230
18.1  无限族上的时序逻辑	230
18.2  不变式	231
18.3  再次思考Futurebus+	233
18.4  图和网络文法	235
18.5  令牌环族的不确定性结果	242
本章文献注释	244
第19章  离散实时系统和定量时序分析	246
19.1  实时系统和单调变化率调度	246
19.2  实时系统的模型检测	247
19.3  RTCTL模型检测	247
19.4  量化时序的分析：最小或最大延迟	248
19.4.1  最小延迟算法	248
19.4.2  最大延迟算法	249
19.5  实例：飞行控制器	250
19.5.1  系统描述	250
19.5.2  飞行控制系统的模型	252
19.5.3  验证结果	252
本章文献注释	254
第20章  连续实时系统	255
20.1  定时自动机	255
20.2  并行组合	257
20.3  使用定时自动机建模	258
20.4  时钟域	260
20.5  时钟区	265
20.6  边界可区分矩阵	270
20.7  复杂度问题	274
本章文献注释	274
原著参考文献	275

序

“推动计算机进一步帮助人类”，让其承担更复杂和关键的任务，其主要的障碍并不是计算机的速度不足和基础算力不佳，这一点大家已经达成了共识；而是缺乏设计和实现所有场景下都保持正确的复杂系统的能力，在这方面我们的确信心不足。
设计核验——尽早确保设计的正确性——是所有规范的系统开发过程的主要挑战，解决这个问题的成本和时间占比，已经在整个开发周期中越来越大。
在大多数场合下，设计核验依然采用传统的模拟和测试技术。在调试的早期阶段，设计中充斥着各种各样的错误，在该阶段已证明这些技术是有效的。但随着设计逐步变清晰，模拟和测试技术的有效性会急剧下降，采用这两类技术时，细微错误暴露的时间长得惊人。从本质上来说，这两类技术的一个严重问题是，人们无法确定二者的工作极限，也无法评估设计中还有多少潜在错误。随着设计的复杂性急剧增加，例如单颗芯片从50万门规模发展到500万门的高级芯片设计，有远见的管理者预见到这些传统方法将彻底崩盘，完全没有继续发展的能力。
本书的主题是形式化验证，此方法是一种替代模拟和测试技术的方案，极具吸引力且越来越受欢迎。模拟和测试探索的是系统某些可能的行为和场景，但无法回答未探索轨迹是否包含致命错误的问题；而形式化验证则穷尽探索系统所有可能的行为。因此，当形式化验证宣称一个设计正确时，意味着所有行为都被探索过，此时讨论覆盖率是否充分或行为是否遗漏，就变得无足轻重了。
这些年来，人们已经提出了多种形式化验证方案。本书专注于模型检测，通过对系统（模型）的所有可达状态及由这些状态构成的行为进行（显式或隐式）穷尽探索，以验证所期望的反应式系统应该具备的行为性质。
与其他方法相比，模型检测方法拥有两大明显的优势。
?	全自动：模型检测不需要用户监督，也不要求用户具备逻辑和定理证明等数理方面的专业知识。任何能对设计进行模拟的人，完全有能力对同一设计进行模型检测。在当前实际使用的流程中，模型检测可被视为一种极其优良的模拟工具。
?	反例：若设计无法满足期望性质，模型检测会产生一个反例，此反例揭示出违反该性质的系统行为。反例提供的错误轨迹非常有利于理解产生错误的真实原因，也为修复设计问题提供了重要线索。
这两大显著优势，再加上能够对海量状态进行隐式穷尽探索的符号模型检测技术，彻底革新了形式化验证，将其从一门纯学术的理论方法转变为一种切实可行的实用技术，使其具有作为设计验证备用方法并被整合到工业开发流程中的潜力。
在大多数先进半导体和处理器制造公司内部，都有大量研究人员和开发人员致力于研发专用模型检测工具及应用范例，充分证明了工业界已经广泛认可模型检测的巨大实用潜力。
非常幸运，终于出现了这本有关模型检测原理和方法的权威专著，本书的作者正是最初构想出模型检测思想的先驱，他们以令人印象深刻的智慧和毅力，持续推动其发展，直至模型检测达到了今天的成就。
我坚信，对于众多关注模型检测这种形式化验证技术的读者和实践者，这本专著能够提供卓越的参考和指南。


Amir Pnueli

本书配套资源下载

对不起，暂无音视频资源！

模型检测（第二版）