书籍详情
模型检测
作者：（美）埃德蒙,·,M.,克拉克 等
出版社：电子工业出版社
出版时间：2018-11-01
ISBN：9787121352744
定价：¥69.00
购买这本书可以去
内容简介
模型检测是一种用于自动验证有限状态并发系统的技术，与基于模拟、测试和演绎推理的传统技术相比，具有许多方面的优势。本书共分18章，涵盖的主要内容包括模型检测的基本知识、模态逻辑、符号化技术、SATSolver、限界模型检测、自动机上的模型检测、抽象解释、程序分析、实时系统验证，同时介绍NuSMV和UPPAAL两个流行的模型检测器。
作者简介
Edmund M.Clarke教授，美国卡内基 ？ 梅隆大学计算机科学系教授，并且是ACM和IEEE会士。他在软硬件验证、自动定理证明、形式方法等方面享有崇高的国际声誉，2007年获得ACM图灵奖。吴尽昭，广西大学副校长，长期从事高效能高可信计算与推理理论与工具的研究和开发，研究领域涉及符号计算、自动推理、形式化方法及其交叉、融合与应用；在国内外学术刊物和国际会议论文集上发表研究论文107篇，出版专著3部，获得软件著作权6项，申请专利3项；近年来承担国家自然科学基金、863、973子课题等国家、省部级科研项目10余项。
目录
目 录
第1章 绪论\t1
1．1 形式化方法的需求\t1
1．2 硬件与软件验证\t1
1．3 模型检测的流程\t3
1．4 时序逻辑与模型检测\t3
1．5 符号算法\t4
1．6 偏序约简\t6
1．7 缓解状态爆炸问题的其他方法\t7
第2章 系统建模\t8
2．1 并发系统建模\t8
2．2 并发系统\t11
2．3 程序翻译的实例\t16
第3章 时序逻辑\t18
3．1 计算树逻辑CTL*\t18
3．2 CTL和LTL逻辑\t20
3．3 公正性\t22
第4章 模型检测\t24
4．1 CTL模型检测\t24
4．2 基于tableau结构的LTL模型检测\t29
4．3 CTL*模型检测\t33
第5章 二叉判定图\t36
5．1 布尔公式的表示方法\t36
5．2 Kripke结构的表示方法\t40
第6章 符号模型检测\t42
6．1 不动点表示\t42
6．2 CTL符号模型检测\t45
6．3 符号模型检测中的公正性\t48
6．4 反例和诊断信息\t50
6．5 一个ALU的例子\t52
6．6 关系积的计算\t54
6．7 符号化的LTL模型检测\t61
第7章 基于? 演算的模型检测\t68
7．1 简介\t68
7．2 命题? 演算\t68
7．3 求不动点公式的值\t71
7．4 用OBDD表示? 演算公式\t74
7．5 将CTL公式转化为? 演算\t75
7．6 复杂度问题\t76
第8章 实践中的模型检测\t77
8．1 SMV模型检测器\t77
8．2 一个实际的例子\t80
第9章 模型检测和自动机理论\t85
9．1 有限字与无限字上的自动机\t85
9．2 使用自动机进行模型检测\t86
9．3 检查Büchi自动机接受的语言是否为空\t90
9．4 LTL公式转化为自动机\t93
9．5 采用“On-the-Fly”技术的模型检测\t97
9．6 检测语言包含的符号方法\t98
第10章 偏序约简\t100
10．1 异步系统中的并发\t101
10．2 独立性与不可见性\t102
10．3 LTL?X的偏序约简\t104
10．4 一个例子\t107
10．5 计算充足集(ample)集合\t109
10．6 算法的正确性\t114
10．7 SPIN系统中的偏序约简\t117
第11章 结构间的等价性和拟序\t122
11．1 等价和拟序算法\t128
11．2 构建tableau结构\t129
第12章 组合推理\t133
12．1 多个结构的组合\t134
12．2 判断假设保证证明方法的正确性\t136
12．3 CPU控制器的验证\t136
第13章 抽象\t139
13．1 影响锥化简\t139
13．2 数值抽象\t141
第14章 对称性\t154
14．1 群和对称性\t154
14．2 商模型\t156
14．3 对称性和模型检测\t159
14．4 复杂度问题\t160
14．5 实验结果\t164
第15章 有限状态系统的无限簇\t166
15．1 无限簇上的时序逻辑\t166
15．2 不变量\t167
15．3 再次分析Futurebus+\t169
15．4 图和网络文法\t171
15．5 令牌环簇的不确定性结果\t179
第16章 离散实时系统和定量时序分析\t183
16．1 实时系统和单调变化率调度\t183
16．2 实时系统的模型检测\t184
16．3 RTCTL模型检测\t185
16．4 量化时序的分析：最小或最大延迟\t185
16．5 飞行控制器\t187
第17章 连续实时系统\t192
17．1 时间约束自动机\t192
17．2 并行组合\t194
17．3 使用时间约束自动机进行建模\t195
17．4 时钟域\t198
17．5 时钟区\t203
17．6 边界可区分矩阵\t208
17．7 复杂度问题\t211
第18章 结论\t213
参考文献\t215
第1章 绪论\t1
1．1 形式化方法的需求\t1
1．2 硬件与软件验证\t1
1．3 模型检测的流程\t3
1．4 时序逻辑与模型检测\t3
1．5 符号算法\t4
1．6 偏序约简\t6
1．7 缓解状态爆炸问题的其他方法\t7
第2章 系统建模\t8
2．1 并发系统建模\t8
2．2 并发系统\t11
2．3 程序翻译的实例\t16
第3章 时序逻辑\t18
3．1 计算树逻辑CTL*\t18
3．2 CTL和LTL逻辑\t20
3．3 公正性\t22
第4章 模型检测\t24
4．1 CTL模型检测\t24
4．2 基于tableau结构的LTL模型检测\t29
4．3 CTL*模型检测\t33
第5章 二叉判定图\t36
5．1 布尔公式的表示方法\t36
5．2 Kripke结构的表示方法\t40
第6章 符号模型检测\t42
6．1 不动点表示\t42
6．2 CTL符号模型检测\t45
6．3 符号模型检测中的公正性\t48
6．4 反例和诊断信息\t50
6．5 一个ALU的例子\t52
6．6 关系积的计算\t54
6．7 符号化的LTL模型检测\t61
第7章 基于? 演算的模型检测\t68
7．1 简介\t68
7．2 命题? 演算\t68
7．3 求不动点公式的值\t71
7．4 用OBDD表示? 演算公式\t74
7．5 将CTL公式转化为? 演算\t75
7．6 复杂度问题\t76
第8章 实践中的模型检测\t77
8．1 SMV模型检测器\t77
8．2 一个实际的例子\t80
第9章 模型检测和自动机理论\t85
9．1 有限字与无限字上的自动机\t85
9．2 使用自动机进行模型检测\t86
9．3 检查Büchi自动机接受的语言是否为空\t90
9．4 LTL公式转化为自动机\t93
9．5 采用“On-the-Fly”技术的模型检测\t97
9．6 检测语言包含的符号方法\t98
第10章 偏序约简\t100
10．1 异步系统中的并发\t101
10．2 独立性与不可见性\t102
10．3 LTL?X的偏序约简\t104
10．4 一个例子\t107
10．5 计算充足集(ample)集合\t109
10．6 算法的正确性\t114
10．7 SPIN系统中的偏序约简\t117
第11章 结构间的等价性和拟序\t122
11．1 等价和拟序算法\t128
11．2 构建tableau结构\t129
第12章 组合推理\t133
12．1 多个结构的组合\t134
12．2 判断假设保证证明方法的正确性\t136
12．3 CPU控制器的验证\t136
第13章 抽象\t139
13．1 影响锥化简\t139
13．2 数值抽象\t141
第14章 对称性\t154
14．1 群和对称性\t154
14．2 商模型\t156
14．3 对称性和模型检测\t159
14．4 复杂度问题\t160
14．5 实验结果\t164
第15章 有限状态系统的无限簇\t166
15．1 无限簇上的时序逻辑\t166
15．2 不变量\t167
15．3 再次分析Futurebus+\t169
15．4 图和网络文法\t171
15．5 令牌环簇的不确定性结果\t179
第16章 离散实时系统和定量时序分析\t183
16．1 实时系统和单调变化率调度\t183
16．2 实时系统的模型检测\t184
16．3 RTCTL模型检测\t185
16．4 量化时序的分析：最小或最大延迟\t185
16．5 飞行控制器\t187
第17章 连续实时系统\t192
17．1 时间约束自动机\t192
17．2 并行组合\t194
17．3 使用时间约束自动机进行建模\t195
17．4 时钟域\t198
17．5 时钟区\t203
17．6 边界可区分矩阵\t208
17．7 复杂度问题\t211
第18章 结论\t213
参考文献\t215
猜您喜欢
