| 摘要 | 第3-4页 |
| Abstract | 第4-5页 |
| 第一章 绪论 | 第8-14页 |
| 1.1 研究背景和意义 | 第8-10页 |
| 1.2 模型检测国内外研究现状 | 第10-11页 |
| 1.3 本文主要的研究内容 | 第11-14页 |
| 第二章 经典模型检测 | 第14-20页 |
| 2.1 模型检测原理 | 第14-15页 |
| 2.2 经典模型检测理论 | 第15-18页 |
| 2.2.1 经典Kripke结构 | 第15-16页 |
| 2.2.2 计算树逻辑(CTL) | 第16-18页 |
| 2.3 小结 | 第18-20页 |
| 第三章 多值可能性测度下的模型检测 | 第20-32页 |
| 3.1 格论和多值逻辑 | 第20-22页 |
| 3.2 多值可能性Kripke结构 | 第22-24页 |
| 3.3 基于可能性测度的多值计算树逻辑及其语义 | 第24-26页 |
| 3.3.1 多值Kripke结构的可能性测度 | 第24-25页 |
| 3.3.2 多值可能性测度的多值计算树逻辑 | 第25-26页 |
| 3.4 基于多值可能性测度的多值计算树逻辑模型检测 | 第26-29页 |
| 3.5 多值计算树逻辑模型检测算法 | 第29-30页 |
| 3.6 小结 | 第30-32页 |
| 第四章 模型检测器的设计与实现 | 第32-44页 |
| 4.1 引言 | 第32页 |
| 4.2 模型检测器的架构设计 | 第32-34页 |
| 4.3 转换器的设计 | 第34-36页 |
| 4.3.1 格值转换器的设计 | 第34-35页 |
| 4.3.2 性质转化器的设计 | 第35-36页 |
| 4.4 模型构建层设计 | 第36页 |
| 4.5 计算层设计 | 第36-42页 |
| 4.5.1 运算函数实现 | 第37-39页 |
| 4.5.2 计算内核实现 | 第39-42页 |
| 4.6 验证层设计 | 第42-43页 |
| 4.7 小结 | 第43-44页 |
| 第五章 模型检测器的验证 | 第44-50页 |
| 5.1 模型检测器的时间性能测试实验 | 第44-45页 |
| 5.2 恒温器性质验证实验 | 第45-48页 |
| 5.3 小结 | 第48-50页 |
| 第六章 总结与展望 | 第50-52页 |
| 6.1 全文总结 | 第50-51页 |
| 6.2 未来工作的展望 | 第51-52页 |
| 参考文献 | 第52-56页 |
| 致谢 | 第56-58页 |
| 攻读硕士期间研究成果 | 第58页 |