基于SPIN的UML模型验证技术的研究
| 摘要 | 第1-4页 |
| Abstract | 第4-8页 |
| 第一章 绪论 | 第8-12页 |
| ·研究背景 | 第8-9页 |
| ·论文的主要工作 | 第9-10页 |
| ·研究目标 | 第9-10页 |
| ·研究内容 | 第10页 |
| ·本论文的组织结构 | 第10-12页 |
| 第二章 模型验证 | 第12-23页 |
| ·模型验证概述 | 第12-14页 |
| ·模型验证的基本概念和原理 | 第12-13页 |
| ·模型验证的过程 | 第13页 |
| ·模型验证优化技术 | 第13-14页 |
| ·时态逻辑 | 第14-16页 |
| ·线性时态逻辑 | 第14-15页 |
| ·分支时态逻辑 | 第15-16页 |
| ·模型验证工具SPIN | 第16-23页 |
| ·PROMELA语言 | 第18-21页 |
| ·系统性质的描述 | 第21-23页 |
| 第三章 UML模型的验证 | 第23-29页 |
| ·UML简介 | 第23-24页 |
| ·UML组成结构 | 第24-25页 |
| ·UML建模 | 第25-26页 |
| ·UML模型的验证 | 第26-29页 |
| 第四章 UML模型到PROMELA模型的转换 | 第29-53页 |
| ·UML验证模型到PROMELA模型的转换方法 | 第29-30页 |
| ·UML状态机的语义描述 | 第30-39页 |
| ·UML状态机的抽象语法 | 第31-34页 |
| ·活动状态配置 | 第34-35页 |
| ·RTC-step语义及模拟执行算法 | 第35-39页 |
| ·UML验证模型在PROMELA中的表示 | 第39-49页 |
| ·UML协作图在PROMELA中的表示 | 第49-50页 |
| ·UML模型到PROMELA模型的转换算法 | 第50-53页 |
| 第五章 UML自动转换验证工具的设计与实现 | 第53-67页 |
| ·工具的体系结构 | 第53-54页 |
| ·工具的设计与实现 | 第54-61页 |
| ·基本数据结构 | 第54-58页 |
| ·工具的核心算法的实现 | 第58-60页 |
| ·工具的用户界面及使用 | 第60-61页 |
| ·实例应用 | 第61-67页 |
| 第六章 总结与展望 | 第67-69页 |
| ·总结 | 第67-68页 |
| ·进一步的工作 | 第68-69页 |
| 参考文献 | 第69-74页 |
| 攻读硕士期间发表的论文 | 第74-75页 |
| 致谢 | 第75页 |
