模型检测

　　模型检测是一种用于自动验证有限状态并发系统的技术，与基于模拟、测试和演绎推理的传统技术相比，具有许多方面的优势。本书涵盖的内容包括模型检测的基本知识、模态逻辑、符号化技术、SAT Solver、限界模型检测、自动机上的模型检测、抽象解释、程序分析、实时系统验证，同时介绍NuSMV和UPPAAL两个流行的模型检测器。

　　李刚，华北电力大学（保定）计算机系讲师，目前从事软件工程、建模与仿真、智能电网的信息化管理等方面的研究工作，主要内容是将计算机科学与技术的理论方法应用到电力系统的问题中，在智电网的故障诊断与预测方面，获得实用新型专利授权2项、计算机软件著作权1项。

目 录第1章 绪论1.1 形式化方法的需求1.2 硬件与软件验证1.3 模型检测的过程1.4 时序逻辑与模型检测1.5 符号算法1.6 偏序约简1.7 缓解状态爆炸问题的其他方法第2章 系统建模2.1 并发系统建模2.2 并发系统2.3 一个并发程序的Kripke模型第3章 时序逻辑3.1 计算树逻辑CLT*3.2 CTL和LTL3.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 模型检测器——SMV8.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章 结论参考文献