书籍详情
模型检验原理
作者：（德）克里斯特尔·拜耳（Christel Baier）
出版社：清华大学出版社
出版时间：2021-11-01
ISBN：9787302577355
定价：¥158.00
购买这本书可以去
内容简介
本书全面系统地介绍了模型检验的一般原理、应用工具及软硬件系统的建模与验证方法，同时介绍了克服模型检验中“状态空间爆炸”问题的有效途径，可作为计算机科学与技术、软件工程等专业本科生、研究生的教材，也可作为模型检验领域研究人员及注重系统可靠性的设计与开发人员的参考书。
作者简介
赵光峰，男，1964年生，教授，博士，曾留学英国一年，主要研究方向为拓扑学、图论、系统可信性自动验证，发表学术论文30余篇，主编《Visual Basic 程序设计教程》（高等教育出版社）等教材5部。
目录
●章 系统验证
1.1 模型检验
1.2 模型检验的特征
1.2.1 模型检验的步骤
1.2.2 模型检验的优点与缺点
1.3 文献说明
第2章 并发系统的建模
2.1 迁移系统
2.1.1 执行
2.1.2 硬件和软件系统的建模
2.2 并行与通信
2.2.1 并发与交错
2.2.2 用共享变量通信
2.2.3 握手
2.2.4 通道系统
2.2.5 nanoPromela
2.2.6 同步并行性
2.3 状态空间爆炸问题
2.4 总结
2.5 文献说明
2.6 习题
第3章 线性时间性质
3.1 死锁
3.2 线性时间行为
3.2.1 路径与状态图
3.2.2 迹
3.2.3 线性时间性质
3.2.4 迹等价与线性时间性质
3.3 安全性质与不变式
3.3.1 不变式
3.3.2 安伞件质
3.3.3 迹等价与安全性质
3.4 活性性质
3.4.1 活性性质概念
3.4.2 安全性质与活性性质
3.5 公平性
3.5.1 公平性约束
3.5.2 公平性策略
3.5.3 公平性与安全性
3.6 总结
3.7 文献说明
3.8 习题
第4章 正则性质
4.1 有限单词上的自动机
4.2 正则安全性质的模型检验
4.2.1 正则安全性质
4.2.2 验证正则安全性质
4.3 无限单词上的自动机
4.3.1 ω正则语言与性质
4.3.2 未定Buchi自动机
4.3.3 确定Buchi自动机
4.3.4 广义未定Buchi自动机
4.4 模型检验ω正则性质
4.4.1 持久性质与乘积
4.4.2 嵌套深度优先搜索
4.5 总结
4.6 文献说明
4.7 习题
第5章 线性时序逻辑
5.1 线性时序逻辑述要
5.1.1 语法
5.1.2 语义
5.1.3 准述性质
5.1.4 LTL公式的等价性
5.1.5 弱直到、释放和正范式
5.1.6 LTL中的公平性
5.2 基于自动机的LTL模型检验
5.2.1 LTL模型检验问题的复杂度
5.2.2 LTL可满足性和有效性检验
5.3 总结
5.4 文献说明
5.5 习题
第6章 计算树逻辑
6.1 引言
6.2 计算树逻辑
6.2.1 语法
6.2.2 语义
6.2.3 CTL公式的等价性
6.2.4 CTL范式
6.3 LTL与CTL的表达力对比
CTL模型检验
.1 基本算法
.2 直到和存在总是运算符
.3 时间复杂度和空间复杂度
6.5 CTL的公平性
6.6 反例和证据
6.6.1 CTL中的反例
6.6.2 公平CTL中的反例和证据
6.7 符号CTL模型检验
6.7.1 开关函数
6.7.2 用开关函数编码迁移系统
6.7.3 有序二决策图
6.7.4 实现基于ROBDD的算法
6.8 CTL
6.8.1 逻辑、表达力和等价
6.8.2 CTL模型检验
6.9 总结
6.10 文献说明
6.11 习题
第7章 等价和抽象
7.1 互模拟
7.1.1 互模拟商
7.1.2 基于动作的互模拟
7.2 互模拟和CTL等价
7.3 求互模拟商的算法
7.3.1 确定初始划分
7.3.2 细化划分
7.3.3 个划分细化算法
7.3.4 效率改进
7.3.5 迁移系统的等价检验
7.4 模拟关系
7.4.1 模拟等价
7.4.2 互模拟、模拟与迹等价
7.5 模拟等价和CTL等价
7.6 求模拟商的算法
7.7 踏步线性时间关系
7.7.1 踏步迹等价
7.7.2 踏步迹等价和LTLO等价
7.8 踏步互模拟
7.8.1 发散敏感的踏步互模拟
7.8.2 赋范互模拟
7.8.3 踏步互模拟和CTLO等价
7.8.4 踏步互模拟求商
7.9 总结
7.10 文献说明
7.11 习题
第8章 偏序约简
8.1 动作的无关性
8.2 线性时间的充足集方法
8.2.1 充足集的条件
8.2.2 动态偏序约简
8.2.3 计算充足集
8.2.4 静态偏序约简
8.3 分支时间的充足集方法
8.4 总结
8.5 文献说明
8.6 习题
第9章 时控自动机
9.1 时控自动机述要
9.1.1 语义
9.1.2 时间发散、时间锁定和芝诺性
9.2 时控计算树逻辑
9.3 TCTL模型检验
9.3.1 消去时间参数
9.3.2 区域迁移系统
9.3.3 TCTL模型检验算法
9.4 总结
9.5 文献说明
9.6 习题
0章 概率系统
10.1 马尔可夫链
10.1.1 可达性概率
10.1.2 定性性质
10.2 概率计算树逻辑
10.2.1 PCTL模型检验
10.2.2 PCTL的定性片段
10.3 线性时间性质
10.4 PCTL和概率互模拟
10.4.1 PCTL
10.4.2 概率互模拟
10.5 带成本的马尔可夫链
10.5.1 成本有界可达性
10.5.2 长远性质
10.6 马尔可夫决策过程
10.6.1 可达性概率
10.6.2 PCTL模型检验
10.6.3 极限性质
10. 线性时间性质和PCTL
10.6.5 公平性
10.7 总结
10.8 文献说明
10.9 习题
附录A 预备知识
A.1 常用符号与记号
A.2 形式语言
A.3 命题逻辑 ……
1.1 模型检验
1.2 模型检验的特征
1.2.1 模型检验的步骤
1.2.2 模型检验的优点与缺点
1.3 文献说明
第2章 并发系统的建模
2.1 迁移系统
2.1.1 执行
2.1.2 硬件和软件系统的建模
2.2 并行与通信
2.2.1 并发与交错
2.2.2 用共享变量通信
2.2.3 握手
2.2.4 通道系统
2.2.5 nanoPromela
2.2.6 同步并行性
2.3 状态空间爆炸问题
2.4 总结
2.5 文献说明
2.6 习题
第3章 线性时间性质
3.1 死锁
3.2 线性时间行为
3.2.1 路径与状态图
3.2.2 迹
3.2.3 线性时间性质
3.2.4 迹等价与线性时间性质
3.3 安全性质与不变式
3.3.1 不变式
3.3.2 安伞件质
3.3.3 迹等价与安全性质
3.4 活性性质
3.4.1 活性性质概念
3.4.2 安全性质与活性性质
3.5 公平性
3.5.1 公平性约束
3.5.2 公平性策略
3.5.3 公平性与安全性
3.6 总结
3.7 文献说明
3.8 习题
第4章 正则性质
4.1 有限单词上的自动机
4.2 正则安全性质的模型检验
4.2.1 正则安全性质
4.2.2 验证正则安全性质
4.3 无限单词上的自动机
4.3.1 ω正则语言与性质
4.3.2 未定Buchi自动机
4.3.3 确定Buchi自动机
4.3.4 广义未定Buchi自动机
4.4 模型检验ω正则性质
4.4.1 持久性质与乘积
4.4.2 嵌套深度优先搜索
4.5 总结
4.6 文献说明
4.7 习题
第5章 线性时序逻辑
5.1 线性时序逻辑述要
5.1.1 语法
5.1.2 语义
5.1.3 准述性质
5.1.4 LTL公式的等价性
5.1.5 弱直到、释放和正范式
5.1.6 LTL中的公平性
5.2 基于自动机的LTL模型检验
5.2.1 LTL模型检验问题的复杂度
5.2.2 LTL可满足性和有效性检验
5.3 总结
5.4 文献说明
5.5 习题
第6章 计算树逻辑
6.1 引言
6.2 计算树逻辑
6.2.1 语法
6.2.2 语义
6.2.3 CTL公式的等价性
6.2.4 CTL范式
6.3 LTL与CTL的表达力对比
CTL模型检验
.1 基本算法
.2 直到和存在总是运算符
.3 时间复杂度和空间复杂度
6.5 CTL的公平性
6.6 反例和证据
6.6.1 CTL中的反例
6.6.2 公平CTL中的反例和证据
6.7 符号CTL模型检验
6.7.1 开关函数
6.7.2 用开关函数编码迁移系统
6.7.3 有序二决策图
6.7.4 实现基于ROBDD的算法
6.8 CTL
6.8.1 逻辑、表达力和等价
6.8.2 CTL模型检验
6.9 总结
6.10 文献说明
6.11 习题
第7章 等价和抽象
7.1 互模拟
7.1.1 互模拟商
7.1.2 基于动作的互模拟
7.2 互模拟和CTL等价
7.3 求互模拟商的算法
7.3.1 确定初始划分
7.3.2 细化划分
7.3.3 个划分细化算法
7.3.4 效率改进
7.3.5 迁移系统的等价检验
7.4 模拟关系
7.4.1 模拟等价
7.4.2 互模拟、模拟与迹等价
7.5 模拟等价和CTL等价
7.6 求模拟商的算法
7.7 踏步线性时间关系
7.7.1 踏步迹等价
7.7.2 踏步迹等价和LTLO等价
7.8 踏步互模拟
7.8.1 发散敏感的踏步互模拟
7.8.2 赋范互模拟
7.8.3 踏步互模拟和CTLO等价
7.8.4 踏步互模拟求商
7.9 总结
7.10 文献说明
7.11 习题
第8章 偏序约简
8.1 动作的无关性
8.2 线性时间的充足集方法
8.2.1 充足集的条件
8.2.2 动态偏序约简
8.2.3 计算充足集
8.2.4 静态偏序约简
8.3 分支时间的充足集方法
8.4 总结
8.5 文献说明
8.6 习题
第9章 时控自动机
9.1 时控自动机述要
9.1.1 语义
9.1.2 时间发散、时间锁定和芝诺性
9.2 时控计算树逻辑
9.3 TCTL模型检验
9.3.1 消去时间参数
9.3.2 区域迁移系统
9.3.3 TCTL模型检验算法
9.4 总结
9.5 文献说明
9.6 习题
0章 概率系统
10.1 马尔可夫链
10.1.1 可达性概率
10.1.2 定性性质
10.2 概率计算树逻辑
10.2.1 PCTL模型检验
10.2.2 PCTL的定性片段
10.3 线性时间性质
10.4 PCTL和概率互模拟
10.4.1 PCTL
10.4.2 概率互模拟
10.5 带成本的马尔可夫链
10.5.1 成本有界可达性
10.5.2 长远性质
10.6 马尔可夫决策过程
10.6.1 可达性概率
10.6.2 PCTL模型检验
10.6.3 极限性质
10. 线性时间性质和PCTL
10.6.5 公平性
10.7 总结
10.8 文献说明
10.9 习题
附录A 预备知识
A.1 常用符号与记号
A.2 形式语言
A.3 命题逻辑 ……
猜您喜欢
