| 摘要 | 第5-6页 |
| ABSTRACT | 第6页 |
| 第一章 引言 | 第11-17页 |
| 1.1 研究背景与动机 | 第11-13页 |
| 1.2 国内外研究现状 | 第13-14页 |
| 1.3 本文主要工作及结构 | 第14-17页 |
| 第二章 技术背景概述 | 第17-25页 |
| 2.1 多线程离散事件模拟语言 | 第17-20页 |
| 2.2 Hoare Logic | 第20-23页 |
| 2.3 本章小结 | 第23-25页 |
| 第三章 基于Trace的实时性Hoare Logic | 第25-35页 |
| 3.1 基于离散时间的语义模型 | 第26-29页 |
| 3.1.1 符号定义与术语 | 第26-28页 |
| 3.1.2 基于离散时间的语义模型 | 第28-29页 |
| 3.2 实时性Hoare Logic | 第29-33页 |
| 3.3 本章小结 | 第33-35页 |
| 第四章 多线程离散事件模拟语言的证明推理系统 | 第35-55页 |
| 4.1 基本定义与术语 | 第36-37页 |
| 4.2 基本推理规则 | 第37-39页 |
| 4.3 顺序程序推理规则 | 第39-42页 |
| 4.4 并发程序推理规则 | 第42-49页 |
| 4.4.1 并发模型 | 第42-45页 |
| 4.4.2 并行程序规则 | 第45-49页 |
| 4.5 结构性语句规则和辅助规则 | 第49-52页 |
| 4.5.1 结构性语句规则 | 第49-51页 |
| 4.5.2 辅助规则 | 第51-52页 |
| 4.6 本章小结 | 第52-55页 |
| 第五章 证明推理系统的可靠性验证与应用 | 第55-69页 |
| 5.1 可靠性 | 第55-65页 |
| 5.1.1 迁移系统 | 第55-56页 |
| 5.1.2 可靠性定义 | 第56-58页 |
| 5.1.3 操作语义 | 第58-59页 |
| 5.1.4 可靠性证明 | 第59-65页 |
| 5.2 证明系统的应用 | 第65-68页 |
| 5.3 本章小结 | 第68-69页 |
| 第六章 总结与展望 | 第69-71页 |
| 6.1 本文总结 | 第69-70页 |
| 6.2 工作展望 | 第70-71页 |
| 参考文献 | 第71-76页 |
| 致谢 | 第76-77页 |
| 硕士学位期间发表论文和参与科研情况 | 第77页 |