基于模型检测的可诊断性的形式化检验研究
| 第一章 引言 | 第1-9页 |
| ·研究背景 | 第7页 |
| ·本文主要内容 | 第7-9页 |
| 第二章 模型检测 | 第9-20页 |
| ·与其它形式检验方法的比较 | 第9-10页 |
| ·模型检测方法的步骤 | 第10-11页 |
| ·Kripke 结构 | 第11页 |
| ·系统建模 | 第11-20页 |
| ·一阶逻辑表示 | 第12-14页 |
| ·变迁粒度 | 第14-15页 |
| ·并发系统建模 | 第15-20页 |
| 第三章 时序逻辑的概述 | 第20-29页 |
| ·CTL*计算树逻辑 | 第20-23页 |
| ·基本概念 | 第21-22页 |
| ·关于Kripke结构的CTL*语义 | 第22-23页 |
| ·CTL 和LTL | 第23-26页 |
| ·CTL | 第24-25页 |
| ·LTL | 第25-26页 |
| ·CTL*，CTL 和LTL 的关系 | 第26-27页 |
| ·合理性约束 | 第27-29页 |
| 第四章 模型检测问题的实现 | 第29-42页 |
| ·CTL 模型检测 | 第29-35页 |
| ·一般实现方法 | 第29-34页 |
| ·基于合理性约束的实现 | 第34-35页 |
| ·LTL 模型检测 | 第35-42页 |
| 第五章 可诊断性的形式化检验 | 第42-53页 |
| ·简介 | 第42页 |
| ·基本假设 | 第42-45页 |
| ·可诊断性 | 第45-47页 |
| ·耦合孪生设备 | 第47-50页 |
| ·基于模型检测的可诊断性 | 第50-52页 |
| ·可诊断性的Kripke 结构 | 第50-51页 |
| ·符号表示法 | 第51页 |
| ·时序逻辑的应用 | 第51-52页 |
| ·结论 | 第52-53页 |
| 第六章 总结与展望 | 第53-54页 |
| 参考文献 | 第54-56页 |
| 摘要 | 第56-59页 |
| Abstract | 第59-62页 |
| 致谢 | 第62-63页 |
| 导师及作者简介 | 第63页 |
