图书介绍
模型检测pdf电子书版本下载
- （美）EDMUND M.CLARKE JR.，ORNA GRUMBERG，DORON A.PELED著；李刚，宋雨等译 著
- 出版社： 北京：电子工业出版社
- ISBN：9787121272950
- 出版时间：2015
- 标注页数：223页
- 文件大小：51MB
- 文件页数：235页
- 主题词：自动检测系统
PDF下载
下载说明
模型检测PDF格式电子书版下载
下载的文件为RAR压缩包。需要使用解压软件进行解压得到PDF格式图书。建议使用BT下载工具Free Download Manager进行下载,简称FDM(免费,没有广告,支持多平台）。本站资源全部打包为BT种子。所以需要使用专业的BT下载软件进行下载。如 BitComet qBittorrent uTorrent等BT下载工具。迅雷目前由于本站不是热门资源。不推荐使用！后期资源热门了。安装了迅雷也可以迅雷进行下载！
（文件页数 要大于 标注页数，上中下等多册电子书除外）
注意：本站所有压缩包均有解压码： 点击下载压缩包解压工具
图书目录
第1章 绪论 1
1.1 形式化方法的需求 1
1.2 硬件与软件验证 1
1.3 模型检测的过程 3
1.4 时序逻辑与模型检测 3
1.5 符号算法 5
1.6 偏序约简 6
1.7 缓解状态爆炸问题的其他方法 7
第2章 系统建模 9
2.1 并发系统建模 9
2.2 并发系统 12
2.3 一个并发程序的Kripke模型 17
第3章 时序逻辑 19
3.1 计算树逻辑CLT＊ 19
3.2 CTL和LTL 21
3.3 公正性 23
第4章 模型检测 25
4.1 CTL模型检测 25
4.2 用tableau进行LTL模型检测 30
4.3 CTL＊模型检测 34
第5章 二叉判定图 37
5.1 布尔公式的表示方法 37
5.2 Kripke结构的表示方法 41
第6章 符号模型检测 43
6.1 不动点表示 43
6.2 CTL符号模型检测 47
6.3 符号模型检测中的公正性 49
6.4 反例和诊断信息 51
6.5 一个ALU的例子 53
6.6 关系积的计算 55
6.7 符号化的LTL模型检测 62
第7章 基于μ－演算的模型检测 69
7.1 简介 69
7.2 命题μ－演算 70
7.3 求不动点公式的值 72
7.4 用OBDD表示μ－演算公式 75
7.5 将CTL公式转化为μ－演算 76
7.6 复杂度问题 77
第8章 实际中的模型检测 78
8.1 模型检测器——SMV 78
8.2 一个实际的例子 81
第9章 模型检测和自动机理论 86
9.1 有限字与无限字上的自动机 86
9.2 用自动机进行模型检测 87
9.3 检查Büchi自动机接受的语言是否为空 91
9.4 LTL公式转化为自动机 94
9.5 采用“on-the-fly”技术的模型检测 98
9.6 检测语言包含的符号方法 99
第10章 偏序约简 101
10.1 异步系统中的并发 102
10.2 独立性与不可见性 103
10.3 LTL-x的偏序约简 105
10.4 一个例子 108
10.5 计算Ample集合 110
10.6 算法的正确性 115
10.7 SPIN系统中的偏序约简 118
第11章 结构间的等价性和拟序 123
11.1 等价和拟序算法 129
11.2 构建tableau结构 130
第12章 组合推理 134
12.1 结构的组合 135
12.2 假设保证方法的证明 136
12.3 CPU控制器的验证 137
第13章 抽象 139
13.1 影响锥化简 139
13.2 数值抽象 141
第14章 对称性 153
14.1 群和对称性 153
14.2 商模型 156
14.3 对称性和模型检测 158
14.4 复杂性问题 159
14.5 试验结果 163
第15章 有限状态系统的无限簇 165
15.1 无限簇上的时序逻辑 165
15.2 不变量 166
15.3 再次分析Futurebus＋ 168
15.4 图和网络文法 170
15.5 令牌环簇的不确定性结果 178
第16章 离散实时系统和定量时序分析 182
16.1 实时系统和单调变化率调度 182
16.2 实时系统的模型检测 183
16.3 RTCTL模型检测 184
16.4 量化时序的分析：最小或最大延迟 184
16.5 飞行控制器 186
第17章 连续实时系统 191
17.1 时间约束自动机 191
17.2 并行组合 193
17.3 使用时间约束自动机进行建模 194
17.4 时钟域 197
17.5 时钟区 202
17.6 边界可区分矩阵 207
17.7 对复杂度的考虑 210
第18章 结论 211
参考文献 213