-
内容大纲
模型检测是一种用于自动验证有限状态并发系统的技术,与基于模拟、测试和演绎推理的传统技术相比,具有许多方面的优势。Edmund M.Clarke,Orna Grumberg,Doron A.Peled著的《模型检测》共分18章,涵盖的主要内容包括模型检测的基本知识、系统建模、时序逻辑、符号模型检测技术、SMV模型检测器、模型检测与自动机理论、偏序约简、抽象解释、有限状态系统的无限簇、实时系统验证等。
本书既适合从事计算机科学、电子科学、电气工程、工业制造等复杂系统研究的科研人员阅读,也适合系统管理、测试部门的企事业单位人员作为参考用书。 -
作者介绍
Edmund M.Clarke教授,美国卡内基·梅隆大学计算机科学系教授,并且是ACM和IEEE会士。他在软硬件验证、自动定理证明、形式方法等方面享有崇高的国际声誉,2007年获得ACM图灵奖。 -
目录
第1章 绪论
1.1 形式化方法的需求
1.2 硬件与软件验证
1.3 模型检测的流程
1.4 时序逻辑与模型检测
1.5 符号算法
1.6 偏序约简
1.7 缓解状态爆炸问题的其他方法
第2章 系统建模
2.1 并发系统建模
2.2 并发系统
2.3 程序翻译的实例
第3章 时序逻辑
3.1 计算树逻辑CTL
3.2 CTL和LTL逻辑
3.3 公正性
第4章 模型检测
4.1 CTL模型检测
4.2 基于tableau结构的LTL模型检测
4.3 CTL模型检测
第5章 二叉判定图
5.1 布尔公式的表示方法
5.2 Kripke结构的表示方法
第6章 符号模型检测
6.1 不动点表示
6.2 CTL符号模型检测
6.3 符号模型检测中的公正性
6.4 反例和诊断信息
6.5 一个ALU的例子
6.6 关系积的计算
6.7 符号化的LTL模型检测
第7章 基于μ演算的模型检测
7.1 简介
7.2 命题μ演算
7.3 求不动点公式的值
7.4 用OBDD表示μ演算公式
7.5 将CTL公式转化为μ演算
7.6 复杂度问题
第8章 实践中的模型检测
8.1 SMV模型检测器
8.2 一个实际的例子
第9章 模型检测和自动机理论
9.1 有限字与无限字上的自动机
9.2 使用自动机进行模型检测
9.3 检查Büchi自动机接受的语言是否为空
9.4 LTL公式转化为自动机
9.5 采用“On-the-Fly”技术的模型检测
9.6 检测语言包含的符号方法
第10章 偏序约简
10.1 异步系统中的并发
10.2 独立性与不可见性
10.3 LTL-X的偏序约简
10.4 一个例子
10.5 计算充足集(ample)集合
10.6 算法的正确性
10.7 SPIN系统中的偏序约简
第11章 结构间的等价性和拟序
11.1 等价和拟序算法
11.2 构建tableau结构
第12章 组合推理
12.1 多个结构的组合
12.2 判断假设保证证明方法的正确性
12.3 CPU控制器的验证
第13章 抽象
13.1 影响锥化简
13.2 数值抽象
第14章 对称性
14.1 群和对称性
14.2 商模型
14.3 对称性和模型检测
14.4 复杂度问题
14.5 实验结果
第15章 有限状态系统的无限簇
15.1 无限簇上的时序逻辑
15.2 不变量
15.3 再次分析Futurebus+
15.4 图和网络文法
15.5 令牌环簇的不确定性结果
第16章 离散实时系统和定量时序分析
16.1 实时系统和单调变化率调度
16.2 实时系统的模型检测
16.3 RTCTL模型检测
16.4 量化时序的分析:最小或最大延迟
16.5 飞行控制器
第17章 连续实时系统
17.1 时间约束自动机
17.2 并行组合
17.3 使用时间约束自动机进行建模
17.4 时钟域
17.5 时钟区
17.6 边界可区分矩阵
17.7 复杂度问题
第18章 结论
参考文献
同类热销排行榜
- C语言与程序设计教程(高等学校计算机类十二五规划教材)16
- 电机与拖动基础(教育部高等学校自动化专业教学指导分委员会规划工程应用型自动化专业系列教材)13.48
- 传感器与检测技术(第2版高职高专电子信息类系列教材)13.6
- ASP.NET项目开发实战(高职高专计算机项目任务驱动模式教材)15.2
- Access数据库实用教程(第2版十二五职业教育国家规划教材)14.72
- 信号与系统(第3版下普通高等教育九五国家级重点教材)15.08
- 电气控制与PLC(普通高等教育十二五电气信息类规划教材)17.2
- 数字电子技术基础(第2版)17.36
- VB程序设计及应用(第3版十二五职业教育国家规划教材)14.32
- Java Web从入门到精通(附光盘)/软件开发视频大讲堂27.92
推荐书目
-
孩子你慢慢来/人生三书 华人世界率性犀利的一枝笔,龙应台独家授权《孩子你慢慢来》20周年经典新版。她的《...
-
时间简史(插图版) 相对论、黑洞、弯曲空间……这些词给我们的感觉是艰深、晦涩、难以理解而且与我们的...
-
本质(精) 改革开放40年,恰如一部四部曲的年代大戏。技术突变、产品迭代、产业升级、资本对接...