模型检验原理
全新正版 极速发货
￥ 99.9 6.3折 ￥ 158 全新
仅1件
广东广州
认证卖家担保交易快速发货售后保障
作者(德)克里斯特尔·拜耳,(德)乔斯特-皮尔特·卡托恩
出版社清华大学出版社
ISBN9787302577355
出版时间2021-11
装帧平装
开本16开
定价158元
货号1202553725
上书时间2024-08-06
商品详情
- 品相描述：全新
- 商品描述
-
作者简介
赵光峰，男，1964年生，教授，博士，曾留学英国一年，主要研究方向为拓扑学、图论、系统可信性自动验证，发表学术论文30余篇，主编《Visual Basic 程序设计教程》（高等教育出版社）等教材5部。
目录
第1章系统验证1
1.1模型检验4
1.2模型检验的特征7
1.2.1模型检验的步骤7
1.2.2模型检验的优点与缺点9
1.3文献说明10
第2章并发系统的建模12
2.1迁移系统12
2.1.1执行15
2.1.2硬件和软件系统的建模16
2.2并行与通信23
2.2.1并发与交错23
2.2.2用共享变量通信26
2.2.3握手32
2.2.4通道系统36
2.2.5nanoPromela42
2.2.6同步并行性51
2.3状态空间爆炸问题53
2.4总结55
2.5文献说明55
2.6习题56
第3章线性时间性质61
3.1死锁61
3.2线性时间行为64
3.2.1路径与状态图64
3.2.2迹66
3.2.3线性时间性质68
3.2.4迹等价与线性时间性质71
3.3安全性质与不变式72
3.3.1不变式73
3.3.2安全性质76
3.3.3迹等价与安全性质79
3.4活性性质82
3.4.1活性性质概念82
3.4.2安全性质与活性性质83
3.5公平性86
3.5.1公平性约束87
3.5.2公平性策略93
3.5.3公平性与安全性94
3.6总结96
3.7文献说明97
3.8习题97
第4章正则性质103
4.1有限单词上的自动机103
4.2正则安全性质的模型检验108
4.2.1正则安全性质108
4.2.2验证正则安全性质111
4.3无限单词上的自动机116
4.3.1w正则语言与性质116
4.3.2未定Büchi自动机118
4.3.3确定Büchi自动机128
4.3.4广义未定Büchi自动机131
4.4模型检验w正则性质136
4.4.1持久性质与乘积136
4.4.2嵌套深度优先搜索140
4.5总结149
4.6文献说明149
4.7习题150
第5章线性时序逻辑157
5.1线性时序逻辑述要157
5.1.1语法158
5.1.2语义161
5.1.3准述性质164
5.1.4LTL公式的等价性170
5.1.5弱直到、释放和正范式173
5.1.6LTL中的公平性177
5.2基于自动机的LTL模型检验186
5.2.1LTL模型检验问题的复杂度199
5.2.2LTL可满足性和有效性检验205
5.3总结207
5.4文献说明208
5.5习题208
第6章计算树逻辑218
6.1引言218
6.2计算树逻辑220
6.2.1语法220
6.2.2语义222
6.2.3CTL公式的等价性229
6.2.4CTL范式230
6.3LTL与CTL的表达力对比232
6.4CTL模型检验236
6.4.1基本算法236
6.4.2直到和存在总是运算符241
6.4.3时间复杂度和空间复杂度246
6.5CTL的公平性249
6.6反例和证据259
6.6.1CTL中的反例261
6.6.2公平CTL中的反例和证据264
6.7符号CTL模型检验265
6.7.1开关函数265
6.7.2用开关函数编码迁移系统268
6.7.3有序二叉决策图273
6.7.4实现基于ROBDD的算法283
6.8CTL*294
6.8.1逻辑、表达力和等价294
6.8.2CTL*模型检验298
6.9总结300
6.10文献说明301
6.11习题302
第7章等价和抽象314
7.1互模拟315
7.1.1互模拟商319
7.1.2基于动作的互模拟325
7.2互模拟和CTL*等价327
7.3求互模拟商的算法332
7.3.1确定初始划分334
7.3.2细化划分334
7.3.3个划分细化算法339
7.3.4效率改进340
7.3.5迁移系统的等价检验345
7.4模拟关系347
7.4.1模拟等价353
7.4.2互模拟、模拟与迹等价357
7.5模拟等价和\forallCTL*等价360
7.6求模拟商的算法364
7.7踏步线性时间关系369
7.7.1踏步迹等价370
7.7.2踏步迹等价和LTL_\setminus\bigcirc等价373
7.8踏步互模拟374
7.8.1发散敏感的踏步互模拟379
7.8.2赋范互模拟385
7.8.3踏步互模拟和CTL*_\setminus\bigcirc等价391
7.8.4踏步互模拟求商396
7.9总结404
7.10文献说明404
7.11习题405
第8章偏序约简414
8.1动作的无关性415
8.2线性时间的充足集方法421
8.2.1充足集的条件421
8.2.2动态偏序约简431
8.2.3计算充足集436
8.2.4静态偏序约简442
8.3分支时间的充足集方法452
8.4总结460
8.5文献说明461
8.6习题461
第9章时控自动机469
9.1时控自动机述要471
9.1.1语义476
9.1.2时间发散、时间锁定和芝诺性481
9.2时控计算树逻辑486
9.3TCTL模型检验491
9.3.1消去时间参数492
9.3.2区域迁移系统494
9.3.3TCTL模型检验算法511
9.4总结515
9.5文献说明515
9.6习题516
第10章概率系统520
10.1马尔可夫链521
10.1.1可达性概率530
10.1.2定性性质539
10.2概率计算树逻辑546
10.2.1PCTL模型检验549
10.2.2PCTL的定性片段551
10.3线性时间性质557
10.4PCTL*和概率互模拟565
10.4.1PCTL*565
10.4.2概率互模拟566
10.5带成本的马尔可夫链572
10.5.1成本有界可达性573
10.5.2长远性质580
10.6马尔可夫决策过程584
10.6.1可达性概率597
10.6.2PCTL模型检验608
10.6.3极限性质611
10.6.4线性时间性质和PCTL*619
10.6.5公平性622
10.7总结630
10.8文献说明632
10.9习题633
附录A预备知识641
A.1常用符号与记号641
A.2形式语言643
A.3命题逻辑645
A.4图论649
A.5计算复杂度652
参考文献656
译注680
内容摘要
模型检验是一种对软件和硬件系统的可靠性进行自动验证的形式化技术。使用这种技术，可以自动验证和排除正在开发的系统投入使用后是否存在影响系统安全运行的微小瑕疵。本书全面、系统、详细地介绍了模型检验的逻辑和理论基础、原理、验证工具的使用方法以及软件和硬件系统的建模与验证方法，主要内容包括系统验证、并发系统的建模、线性时间性质、正则性质、线性时序逻辑、计算树逻辑、等价和抽象、偏序约简、时控自动机和概率系统等10章。本书可作为计算机科学与技术、软件工程、电子信息科学与技术及相关专业本科生、研究生的教材，也可作为模型检验领域研究人员及关注系统可靠性的设计与开发人员的参考书。
主编推荐
"1．内容全面，条理系统。
2．实例丰富，便于理解。
3．理论充实，实践性强
4．文献翔实，脉络清晰。
5．习题充足，利于掌握。
6．附录凝练，入门快速。"
相关推荐
— 没有更多了 —
以下为对购买帮助不大的评价