基于懒惰切片的模型检测技术研究
| 摘要 | 第1-7页 |
| Abstract | 第7-10页 |
| 目录 | 第10-12页 |
| 第1章 绪论 | 第12-33页 |
| ·研究背景及意义 | 第12-13页 |
| ·国内外研究现状 | 第13-30页 |
| ·形式化验证 | 第13-15页 |
| ·模型检测 | 第15-24页 |
| ·状态空间缩减 | 第24-29页 |
| ·反例理解 | 第29-30页 |
| ·主要研究内容 | 第30-31页 |
| ·论文组织结构 | 第31-33页 |
| 第2章 基于不动点计算的知识库建模方法 | 第33-44页 |
| ·静态建模方法及其不足 | 第33-34页 |
| ·条件迁移系统 | 第34-36页 |
| ·相关定义 | 第34-35页 |
| ·条件迁移 | 第35页 |
| ·条件迁移系统 | 第35-36页 |
| ·基于不动点计算的建模方法 | 第36-42页 |
| ·CTS 构造函数 | 第36-39页 |
| ·最小不动点计算 | 第39-41页 |
| ·算法分析 | 第41-42页 |
| ·实验结果与分析 | 第42-43页 |
| ·本章小结 | 第43-44页 |
| 第3章 基于懒惰切片的状态空间搜索方法 | 第44-79页 |
| ·基本思想和实例 | 第44-52页 |
| ·基本思想 | 第44-45页 |
| ·基本步骤和实例 | 第45-52页 |
| ·懒惰切片算法 | 第52-70页 |
| ·过近似切片计算 | 第52-57页 |
| ·伪反例判定 | 第57-59页 |
| ·细化局部切片 | 第59-60页 |
| ·懒惰搜索算法 | 第60-68页 |
| ·一种优化的过近似切片 | 第68-70页 |
| ·算法分析 | 第70-73页 |
| ·正确性 | 第70-71页 |
| ·可终止性 | 第71-72页 |
| ·计算代价 | 第72-73页 |
| ·实验结果 | 第73-78页 |
| ·本章小结 | 第78-79页 |
| 第4章 懒惰切片的扩展算法 | 第79-98页 |
| ·基于懒惰切片的 LTL 模型检测算法 | 第79-86页 |
| ·基本 LTL 模型检测算法 | 第79-80页 |
| ·基于懒惰切片的 LTL 模型检测 | 第80-86页 |
| ·懒惰切片与抽象的正交化 | 第86-95页 |
| ·无限状态空间到有限状态空间的抽象 | 第88-90页 |
| ·懒惰切片与谓词抽象的正交化 | 第90-95页 |
| ·实验结果 | 第95-97页 |
| ·本章小结 | 第97-98页 |
| 第5章 基于克雷格插值的反例理解方法 | 第98-106页 |
| ·基于最弱前置条件的反例理解方法 | 第98页 |
| ·相关定义 | 第98-100页 |
| ·反例理解 | 第100-104页 |
| ·计算最弱前置条件 | 第100-101页 |
| ·基于克雷格插值的不一致分析 | 第101-104页 |
| ·基于克雷格插值的反例理解算法 | 第104页 |
| ·实验结果 | 第104-105页 |
| ·本章小结 | 第105-106页 |
| 结论 | 第106-108页 |
| 参考文献 | 第108-117页 |
| 攻读博士学位期间发表的论文和取得的科研成果 | 第117-119页 |
| 致谢 | 第119页 |
