| 摘要 | 第1-6页 |
| ABSTRACT | 第6-11页 |
| 第1章 绪论 | 第11-17页 |
| ·研究背景 | 第11-12页 |
| ·统一建模语言UML | 第11页 |
| ·UML 状态图 | 第11页 |
| ·模型检查 | 第11-12页 |
| ·Spin/Promela | 第12页 |
| ·模型检查状态图的研究现状 | 第12-14页 |
| ·国外的研究 | 第12-13页 |
| ·国内的研究 | 第13-14页 |
| ·本课题的研究内容 | 第14-15页 |
| ·本文组织结构 | 第15-17页 |
| 第2章 形式化分析UML 状态图 | 第17-34页 |
| ·统一建模语言UML | 第17-19页 |
| ·UML 简介 | 第17-18页 |
| ·UML 的目标 | 第18页 |
| ·UML 概念范围及分类 | 第18-19页 |
| ·UML 视图 | 第19页 |
| ·UML 状态机视图 | 第19-28页 |
| ·事件 | 第20-21页 |
| ·状态 | 第21-22页 |
| ·迁移 | 第22-25页 |
| ·复合状态 | 第25-28页 |
| ·伪状态 | 第28页 |
| ·UML 状态图的形式化 | 第28-33页 |
| ·UML 状态图的形式化定义 | 第28-30页 |
| ·操作语义和run-to-completion 步语义 | 第30-33页 |
| ·小结 | 第33-34页 |
| 第3章 模型检查状态图 | 第34-41页 |
| ·模型检查 | 第34-35页 |
| ·线性时序逻辑LTL | 第35页 |
| ·模型检查工具 | 第35-37页 |
| ·模型检查工具Spin | 第35-36页 |
| ·模型检查工具SMV | 第36-37页 |
| ·模型检查状态图的难点 | 第37-38页 |
| ·模型检查状态图的一般方法 | 第38-40页 |
| ·使用SMV 模型检查RSML | 第38页 |
| ·使用SMV 模型检查STATEMATE | 第38页 |
| ·使用 Spin 模型检查 STATEMATE | 第38-39页 |
| ·使用Spin 模型检查UML 状态图 | 第39页 |
| ·使用 vUML 模型检查 UML 状态图 | 第39-40页 |
| ·小结 | 第40-41页 |
| 第4章 UML 状态图模型检查算法 | 第41-46页 |
| ·状态图山脉算法 | 第41-42页 |
| ·迁移提取算法 | 第42-43页 |
| ·转化算法分析 | 第43-45页 |
| ·迁移冲突问题 | 第43-44页 |
| ·层次化问题 | 第44页 |
| ·并发问题 | 第44页 |
| ·通信问题 | 第44页 |
| ·步语义问题 | 第44页 |
| ·事件队列的模拟 | 第44页 |
| ·选择 Spin 作为转化目标 | 第44-45页 |
| ·小结 | 第45-46页 |
| 第5章 SC2Spin 的设计、实现和使用 | 第46-57页 |
| ·SC2Spin 的设计 | 第46-49页 |
| ·SC2Spin 的实现 | 第49-52页 |
| ·SC2Spin 的使用 | 第52-56页 |
| ·小结 | 第56-57页 |
| 第6章 实验 | 第57-76页 |
| ·采用方法一的哲学家就餐问题 | 第57-67页 |
| ·问题描述 | 第57页 |
| ·SC2Spin 生成的代码分析 | 第57-66页 |
| ·验证结果 | 第66-67页 |
| ·采用方法二的哲学家就餐问题 | 第67-73页 |
| ·问题描述 | 第67页 |
| ·SC2Spin 生成的代码分析 | 第67-72页 |
| ·验证结果 | 第72-73页 |
| ·采用方法三的哲学家就餐问题 | 第73页 |
| ·问题描述 | 第73页 |
| ·验证结果 | 第73页 |
| ·囚犯问题 | 第73-74页 |
| ·问题描述 | 第73-74页 |
| ·验证结果 | 第74页 |
| ·小结 | 第74-76页 |
| 结论 | 第76-77页 |
| 参考文献 | 第77-81页 |
| 附录A 攻读学位期间所发表的论文和参加的项目 | 第81-82页 |
| 致谢 | 第82页 |