VIP会员
内容简介
本书系统地介绍了模型检验的一般原理、应用工具及软硬件系统的建模与验证方法，同时介绍了克服模型检验中“状态空间爆炸”问题的有效途径，可作为计算机科学与技术、软件工程等专业本科生、研究生的教材，也可作为模型检验领域研究人员及注重系统可靠的设计与开发人员的参考书。
目录
目 录第1章 系统验证 11.1 模型检验 41.2 模型检验的特征 71.2.1 模型检验的步骤 71.2.2 模型检验的优点与缺点 91.3 文献说明 10第2章 并发系统的建模 122.1 迁移系统 122.1.1 执行 152.1.2 硬件和软件系统的建模 162.2 并行与通信 232.2.1 并发与交错 232.2.2 用共享变量通信 262.2.3 握手 322.2.4 通道系统 362.2.5 nanoPromela 422.2.6 同步并行 512.3 状态空间爆炸问题 532.4 结 552.5 文献说明 552.6 习题 56第3章 线时间质 613.1 死锁 613.2 线时间行为 643.2.1 路径与状态图 643.2.2 迹 663.2.3 线时间质 683.2.4 迹等价与线时间质 713.3 质与不变式 723.3.1 不变式 733.3.2 质 763.3.3 迹等价与质 793.4 活质 823.4.1 活质概念 823.4.2 质与活质 833.5 公平 863.5.1 公平约束 873.5.2 公平策略 933.5.3 公平与 943.6 结 963.7 文献说明 973.8 习题 97第4章 正则质 1034.1 有限单词上的自动机 1034.2 正则质的模型检验 1084.2.1 正则质 1084.2.2 验证正则质 1114.3 无限单词上的自动机 1164.3.1 ??正则语言与质 1164.3.2 未定 Büchi 自动机 1184.3.3 确定 Büchi 自动机 1284.3.4 广义未定 Büchi 自动机 1314.4 模型检验?正则质 1364.4.1 持久质与乘积 1364.4.2 嵌套深度优先搜索 1404.5 结 1494.6 文献说明 1494.7 习题 150第5章 线时序逻辑 1575.1 线时序逻辑述要 1575.1.1 语法 1585.1.2 语义 1615.1.3 准述质 1645.1.4 LTL 公式的等价 1705.1.5 弱直到、释放和正范式 1735.1.6 LTL 中的公平 1775.2 基于自动机的 LTL 模型检验 1865.2.1 LTL 模型检验问题的复杂度 1995.2.2 LTL 可满足和有效检验 2055.3 结 2075.4 文献说明 2085.5 习题 208第6章 计算树逻辑 2186.1 引言 2186.2 计算树逻辑 2206.2.1 语法 2206.2.2 语义 2226.2.3 CTL 公式的等价 2296.2.4 CTL 范式 2306.3 LTL 与 CTL 的表达力对比 2326.4 CTL 模型检验 2366.4.1 基本算法 2366.4.2 直到和存是运算符 2416.4.3 时间复杂度和空间复杂度 2466.5 CTL 的公平 2496.6 反例和证据 2596.6.1 CTL 中的反例 2616.6.2 公平 CTL 中的反例和证据 2646.7 符号 CTL 模型检验 2656.7.1 开关函数 2656.7.2 用开关函数编码迁移系统 2686.7.3 有序二叉决策图 2736.7.4 实现基于 ROBDD 的算法 2836.8 CTL* 2946.8.1 逻辑、表达力和等价 2946.8.2 CTL* 模型检验 2986.9 结 3006.10 文献说明 3016.11 习题 302第7章 等价和抽象 3147.1 互模拟 3157.1.1 互模拟商 3197.1.2 基于动作的互模拟 3257.2 互模拟和CTL* 等价 3277.3 求互模拟商的算法 3327.3.1 确定初始划分 3347.3.2 细化划分 3347.3.3 个划分细化算法 3397.3.4 效率改进 3407.3.5 迁移系统的等价检验 3457.4 模拟关系 3477.4.1 模拟等价 3537.4.2 互模拟、模拟与迹等价 3577.5 模拟等价和\forall CTL*等价 3607.6 求模拟商的算法 3647.7 踏步线时间关系 3697.7.1 踏步迹等价 3707.7.2 踏步迹等价和LTL_\setminuigcirc 等价 3737.8 踏步互模拟 3747.8.1 发散敏感的踏步互模拟 3797.8.2 赋范互模拟 3857.8.3 踏步互模拟和CTL*_\setminuigcirc 等价 3917.8.4 踏步互模拟求商 3967.9 结 4047.10 文献说明 4047.11 习题 405第8章 偏序约简 4148.1 动作的无关 4158.2 线时间的充足集方法 4218.2.1 充足集的条件 4218.2.2 动态偏序约简 4318.2.3 计算充足集 4368.2.4 静态偏序约简 4428.3 分支时间的充足集方法 4528.4 结 4608.5 文献说明 4618.6 习题 461第9章 时控自动机 4699.1 时控自动机述要 4719.1.1 语义 4769.1.2 时间发散、 时间锁定 和芝诺 4819.2 时控计算树逻辑 4869.3 TCTL 模型检验 4919.3.1 消去时间参数 4929.3.2 区域迁移系统 4949.3.3 TCTL 模型检验算法 5119.4 结 5159.5 文献说明 5159.6 习题 516第10章 概率系统 52010.1 马尔可夫链 52110.1.1 可达概率 53010.1.2 定质 53910.2 概率计算树逻辑 54610.2.1 PCTL 模型检验 54910.2.2 PCTL 的定片段 55110.3 线时间质 55710.4 PCTL* 和概率互模拟 56510.4.1 PCTL* 56510.4.2 概率互模拟 56610.5 带成本的马尔可夫链 57210.5.1 成本有界可达 57310.5.2 长远质 58010.6 马尔可夫决策过程 58410.6.1 可达概率 59710.6.2 PCTL 模型检验 60810.6.3 极限质 61110.6.4 线时间质和PCTL* 61910.6.5 公平 62210.7 结 63010.8 文献说明 63210.9 习题 633附录 A 预备知识 641A.1 常用符号与记号 641A.2 形式语言 643A.3 命题逻辑 645A.4 图论 649A.5 计算复杂度 652参考文献 656译注 680