模型检测在配置中的应用
| 提要 | 第1-7页 |
| 第1章 绪 论 | 第7-13页 |
| ·课题的研究背景 | 第7页 |
| ·各种验证方法分析 | 第7-8页 |
| ·模型检测技术的发展与现状 | 第8-11页 |
| ·本文的结构层次 | 第11-13页 |
| 第2章 模型检测理论 | 第13-24页 |
| ·模型检测的概念 | 第13页 |
| ·应用模型检测的过程 | 第13-14页 |
| ·Kripke 结构与一阶逻辑表示 | 第14-16页 |
| ·Kripke 结构 | 第14页 |
| ·一阶公式表示 | 第14-15页 |
| ·一阶公式与Kripke 结构的转化 | 第15-16页 |
| ·时态逻辑 | 第16-20页 |
| ·计算树逻辑（CTL*） | 第16-18页 |
| ·分支时间逻辑（CTL） | 第18-19页 |
| ·线性时态逻辑（LTL） | 第19-20页 |
| ·三种常用时态逻辑公式的模型检测 | 第20-24页 |
| ·CTL 模型检测 | 第20-22页 |
| ·LTL 模型检测 | 第22-23页 |
| ·CTL* 模型检测 | 第23-24页 |
| 第3章 主要模型检测技术 | 第24-38页 |
| ·基于 CTL 的符号化模型检测技术 | 第24-29页 |
| ·不动点表示 | 第24-25页 |
| ·量词布尔公式 | 第25-27页 |
| ·有序二分决策图（OBDD） | 第27-29页 |
| ·有界模型检测技术 | 第29-35页 |
| ·有界模型检测语义描述 | 第29-31页 |
| ·有界模型检测问题表示为SAT 问题 | 第31-33页 |
| ·SAT 求解器的工作原理 | 第33-35页 |
| ·On-The-Fly 模型检测技术 | 第35-38页 |
| ·有限状态自动机与Kripke 结构 | 第35-36页 |
| ·On-The-Fly 模型检测 | 第36-38页 |
| 第4章 模型检测在产品配置中的应用 | 第38-52页 |
| ·产品配置问题相关概念 | 第38-39页 |
| ·配置问题表示为模型检测问题 | 第39-46页 |
| ·配置问题的知识表示 | 第39-40页 |
| ·配置问题建模 | 第40-42页 |
| ·基本约束的处理算法 | 第42-46页 |
| ·基于模型检测的配置实例研究 | 第46-50页 |
| ·电脑产品配置模型检测实例 | 第47-49页 |
| ·实验结果分析 | 第49-50页 |
| ·配置问题中模型检测的实现流程图 | 第50-52页 |
| 第5章 总结和展望 | 第52-53页 |
| ·工作总结 | 第52页 |
| ·下一步工作展望 | 第52-53页 |
| 参考文献 | 第53-56页 |
| 致谢 | 第56-57页 |
| 摘要 | 第57-60页 |
| Abstract | 第60-62页 |
