| 摘要 | 第1-5页 |
| Abstract | 第5-7页 |
| 目录 | 第7-9页 |
| 第1章 引言 | 第9-15页 |
| ·研究的背景和意义 | 第9-11页 |
| ·模型检测技术的研究现状和问题 | 第11-12页 |
| ·主要研究内容 | 第12-13页 |
| ·本文结构及章节安排 | 第13-15页 |
| 第2章 并发系统的模型检测 | 第15-27页 |
| ·并发系统 | 第15页 |
| ·形式化方法概述 | 第15-17页 |
| ·并发系统形式化描述的必要性 | 第15-17页 |
| ·形式化方法研究的主要内容 | 第17页 |
| ·模型检测 | 第17-21页 |
| ·模型检测概述 | 第17-19页 |
| ·模型检测形式化描述方法分类 | 第19-21页 |
| ·模型检测中的状态空间爆炸问题 | 第21-25页 |
| ·本章小结 | 第25-27页 |
| 第3章 基于进程代数的偏序简化技术的研究 | 第27-40页 |
| ·CCS概述 | 第27-30页 |
| ·CCS的基本概念 | 第27-28页 |
| ·CCS的符号和基本算子 | 第28-30页 |
| ·偏序简化技术简介 | 第30-35页 |
| ·独立性和迹 | 第31-33页 |
| ·稳固集(persistent set)和睡眠集(sleep set)技术 | 第33-35页 |
| ·基于进程代数的偏序简化 | 第35-37页 |
| ·本章小结 | 第37-40页 |
| 第4章 基于偏序简化技术模型检测的原型系统实现 | 第40-59页 |
| ·MCTool的设计 | 第40-42页 |
| ·MCTool的系统结构 | 第42-43页 |
| ·模型检测的输入语言MCTL | 第43-47页 |
| ·核心算法实现 | 第47-57页 |
| ·状态化简算法 | 第47-50页 |
| ·安全性验证算法 | 第50-53页 |
| ·死锁性验证算法 | 第53-57页 |
| ·本章小结 | 第57-59页 |
| 第5章 实例研究 | 第59-71页 |
| ·五种典型的进程并发合成模式的简化 | 第59-64页 |
| ·实现对哲学家就餐问题以及资源共享协议的性质验证 | 第64-67页 |
| ·效率分析 | 第67-70页 |
| ·本章小结 | 第70-71页 |
| 第6章 总结与展望 | 第71-73页 |
| 参考文献 | 第73-77页 |
| 攻读学位期间发表论文以及科研情况 | 第77-78页 |
| 致谢 | 第78页 |