| 摘要 | 第1-4页 |
| Abstract | 第4-7页 |
| 第一章 绪论 | 第7-12页 |
| ·UML的发展现状和不足之处 | 第7-8页 |
| ·UML形式化方法分类 | 第8-10页 |
| ·课题的研究内容、方法以及意义 | 第10-11页 |
| ·论文的组织 | 第11-12页 |
| 第二章 UML和Petri网技术 | 第12-22页 |
| ·UML基本内容 | 第12-15页 |
| ·UML的基本定义 | 第12页 |
| ·UML的组成 | 第12-15页 |
| ·Petri网主要知识 | 第15-20页 |
| ·Petri网的相关定义 | 第15-17页 |
| ·Petri网的动态性质 | 第17-19页 |
| ·Petri网的分析方法 | 第19-20页 |
| ·高级Petri网 | 第20-21页 |
| ·小结 | 第21-22页 |
| 第三章 UML的Petri网形式化建模 | 第22-35页 |
| ·UML状态图转换为对象Petri子网 | 第22-25页 |
| ·复合状态转换为简单状态 | 第23-24页 |
| ·简单状态图映射为OPM模型 | 第24-25页 |
| ·UML顺序图的Petri网建模 | 第25-34页 |
| ·UML顺序图的扩展 | 第26-29页 |
| ·扩展的UML顺序图转换为Petri网模型 | 第29-34页 |
| ·小结 | 第34-35页 |
| 第四章 形式化模型的验证分析算法与实现 | 第35-43页 |
| ·可达树算法改进与实现 | 第36-41页 |
| ·利用可达树分析动态行为特征 | 第41-42页 |
| ·小结 | 第42-43页 |
| 第五章 UML形式化建模应用案例 | 第43-51页 |
| ·保险气象评价系统的UML顺序图和状态图形式化模型 | 第45-48页 |
| ·保险气象评价系统的形式化模型的验证与分析工具的实现 | 第48-50页 |
| ·小结 | 第50-51页 |
| 第六章 结论与展望 | 第51-53页 |
| 参考文献 | 第53-57页 |
| 附录 | 第57-58页 |
| 致谢 | 第58-59页 |
| 攻读学位期间参加的科研工作和发表的学术论文 | 第59-60页 |