| 摘要 | 第1-7页 |
| Abstract | 第7-9页 |
| 第1章 绪论 | 第9-11页 |
| ·课题背景 | 第9页 |
| ·主要工作和目标 | 第9-10页 |
| ·论文结构 | 第10-11页 |
| 第2章 形式化验证 | 第11-20页 |
| ·模型检测 | 第11-12页 |
| ·时态逻辑 | 第12-13页 |
| ·Spin工具 | 第13-15页 |
| ·Promela语言 | 第15-20页 |
| 第3章 软件建模 | 第20-29页 |
| ·建模语言 | 第20-22页 |
| ·交互模型 | 第22-29页 |
| 第4章 模型转换算法及软件实现 | 第29-44页 |
| ·顺序图的形式化描述 | 第29-31页 |
| ·转换为 Promela程序 | 第31-35页 |
| ·转换过程的软件实现 | 第35-44页 |
| 第5章 实例分析 | 第44-55页 |
| ·建立 UML顺序图 | 第44-45页 |
| ·解析 XML文档 | 第45-47页 |
| ·生成 Promela程序 | 第47-48页 |
| ·顺序图模拟 | 第48-50页 |
| ·顺序图验证 | 第50-55页 |
| 第6章 结论和下一步工作 | 第55-56页 |
| ·结论 | 第55页 |
| ·下一步工作 | 第55-56页 |
| 参考文献 | 第56-59页 |
| 致谢 | 第59页 |