| 摘要 | 第1-8页 |
| ABSTRACT | 第8-12页 |
| 第一章 引言 | 第12-18页 |
| ·研究背景和意义 | 第12-13页 |
| ·国内外研究现状 | 第13-14页 |
| ·关键问题与技术路线 | 第14-15页 |
| ·主要工作与特色之处 | 第15-16页 |
| ·本文的组织结构 | 第16-18页 |
| 第二章 相关概念介绍 | 第18-21页 |
| ·模型检测 | 第18页 |
| ·模型精化 | 第18-19页 |
| ·EVENT-B模型 | 第19-20页 |
| ·线性时序逻辑(LINEAR TEMPORAL LOGIC,LTL) | 第20页 |
| ·本章小结 | 第20-21页 |
| 第三章 模型系统实例 | 第21-28页 |
| ·模型系统概述 | 第21-22页 |
| ·电烧水壶模型系统 | 第22-26页 |
| ·可能出现的不一致 | 第26-27页 |
| ·本章小结 | 第27-28页 |
| 第四章 模型间一致性检测方法 | 第28-45页 |
| ·基本流程 | 第28-29页 |
| ·抽象测试用例生成 | 第29-32页 |
| ·系统行为属性抽取 | 第32-37页 |
| ·精化关系抽取 | 第37-42页 |
| ·系统行为属性验证 | 第42-43页 |
| ·本章小结 | 第43-45页 |
| 第五章 实验分析 | 第45-49页 |
| ·实验内容 | 第45页 |
| ·实验数据与实验环境 | 第45-47页 |
| ·实验结果分析 | 第47-48页 |
| ·本章小结 | 第48-49页 |
| 第六章 总结与展望 | 第49-52页 |
| ·本文总结 | 第49-50页 |
| ·未来工作展望 | 第50-52页 |
| 附录1 攻读学位期间发表的学术论文目录 | 第52-53页 |
| 附录2 生成的部分线性时序逻辑(LTL)示例 | 第53-56页 |
| 参考文献 | 第56-60页 |
| 致谢 | 第60-61页 |