模型检测

目 录第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章 结论参考文献