需求模型和程序间行为一致性的比较检测
| 论文创新点 | 第1-7页 |
| 摘要 | 第7-9页 |
| Abstract | 第9-11页 |
| 目录 | 第11-13页 |
| 第1章 引言 | 第13-22页 |
| ·研究背景 | 第13-15页 |
| ·研究目的和内容 | 第15-16页 |
| ·相关工作 | 第16-21页 |
| ·历史沿革 | 第16-17页 |
| ·模型比较 | 第17-18页 |
| ·程序分析 | 第18-20页 |
| ·程序抽象 | 第20-21页 |
| ·小结 | 第21页 |
| ·论文组织结构 | 第21-22页 |
| 第2章 比较检测使用的行为模型 | 第22-34页 |
| ·标记迁移系统和操作语义 | 第22-24页 |
| ·模型的特性 | 第23页 |
| ·模型的扩展 | 第23-24页 |
| ·行为描述语言 | 第24-28页 |
| ·行为模型的扩展 | 第26-27页 |
| ·变量和分支条件 | 第27-28页 |
| ·并发状态机 | 第28-33页 |
| ·状态的并发 | 第29-30页 |
| ·并发状态机与Statechart | 第30-31页 |
| ·并发状态机与Petri网 | 第31-32页 |
| ·并发状态机的生成 | 第32-33页 |
| ·本章小结 | 第33-34页 |
| 第3章 程序静态分析和模型提取 | 第34-64页 |
| ·C语言的中间语言及其语义 | 第34-39页 |
| ·C语言程序的生成 | 第34-35页 |
| ·中间语言及其语义 | 第35-37页 |
| ·控制流图及其内联 | 第37-39页 |
| ·函数指针分析 | 第39-53页 |
| ·统一访问路径 | 第39-40页 |
| ·无环约束图 | 第40-41页 |
| ·基于域传播的别名分析 | 第41-46页 |
| ·近似优化 | 第46-49页 |
| ·性能分析 | 第49-52页 |
| ·综合控制流图 | 第52-53页 |
| ·程序行为分析 | 第53-59页 |
| ·数据的抽象 | 第54-55页 |
| ·可观察行为 | 第55-56页 |
| ·行为和数据的对应 | 第56-57页 |
| ·基于可观察行为的程序切片 | 第57-59页 |
| ·程序的并发状态机生成 | 第59-62页 |
| ·并发控制的分析 | 第59-60页 |
| ·从程序控制流到并发状态机 | 第60-62页 |
| ·本章小结 | 第62-64页 |
| 第4章 模型比较检测 | 第64-92页 |
| ·模型的同态 | 第64-77页 |
| ·同构、扩张与收缩 | 第65-67页 |
| ·扩张与精化 | 第67-72页 |
| ·收缩与抽象 | 第72-76页 |
| ·模型同态的小结 | 第76-77页 |
| ·检测方法和技术 | 第77-90页 |
| ·对应关系的搜索 | 第79-83页 |
| ·搜索算法的复杂度 | 第83页 |
| ·分支条件的检查 | 第83-85页 |
| ·差异的分类 | 第85-86页 |
| ·结果的汇总 | 第86-89页 |
| ·模块化检测技术 | 第89-90页 |
| ·本章小结 | 第90-92页 |
| 第5章 模型比较检测的应用 | 第92-105页 |
| ·应用流程 | 第92-98页 |
| ·模型-程序比较分析器——MPCA | 第93-94页 |
| ·对应关系的建立和模型的提取 | 第94-95页 |
| ·比较检测和分析 | 第95-98页 |
| ·实例分析 | 第98-102页 |
| ·实例描述 | 第98-99页 |
| ·差异的分析和修复过程 | 第99-102页 |
| ·其它模型上的比较检测应用 | 第102-104页 |
| ·Statechart的比较检测 | 第102页 |
| ·Petri网的比较检测 | 第102-103页 |
| ·时间自动机的比较检测 | 第103-104页 |
| ·本章小结 | 第104-105页 |
| 第6章 总结和展望 | 第105-107页 |
| ·全文总结 | 第105-106页 |
| ·未来工作展望 | 第106-107页 |
| 参考文献 | 第107-113页 |
| 攻读博士学位期间发表的论文和参与的科研 | 第113-114页 |
| 致谢 | 第114页 |
