| 摘要 | 第1-7页 |
| ABSTRACT | 第7-10页 |
| 第一章 绪论 | 第10-13页 |
| 第一节 研究背景 | 第10-12页 |
| 第二节 论文的主要工作 | 第12页 |
| 第三节 论文组织结构 | 第12-13页 |
| 第二章 统一建模语言UML | 第13-22页 |
| 第一节 UML简介 | 第13-15页 |
| 第二节 UML建模 | 第15-17页 |
| 第三节 UML活动图介绍 | 第17-22页 |
| 第三章 模型验证工具SPIN | 第22-35页 |
| 第一节 模型检测 | 第22-25页 |
| 第二节 SPIN模型检测器 | 第25-29页 |
| 第三节 SPIN的验证过程 | 第29-30页 |
| 第四节 SPIN使用实例 | 第30-34页 |
| 第五节 SPIN小结 | 第34-35页 |
| 第四章 活动图验证系统设计与实现 | 第35-56页 |
| 第一节 验证系统介绍 | 第35-37页 |
| 第二节 层次自动机理论 | 第37-38页 |
| 第三节 活动图验证转换 | 第38-47页 |
| 第四节 活动图模拟 | 第47-56页 |
| 第五章 案例分析 | 第56-63页 |
| 第一节 活动图验证 | 第57-60页 |
| 第二节 活动图模拟 | 第60-63页 |
| 第六章 结束语 | 第63-64页 |
| 参考文献 | 第64-66页 |
| 后记 | 第66页 |