| 摘要 | 第4-5页 |
| Abstract | 第5-6页 |
| 1 绪论 | 第9-13页 |
| 1.1 选题背景和意义 | 第9-10页 |
| 1.2 国内外研究现状 | 第10-11页 |
| 1.3 存在问题和解决方案 | 第11-12页 |
| 1.4 主要研究工作内容 | 第12-13页 |
| 2 等级转换场景和规范描述 | 第13-18页 |
| 2.1 CTCS-3 级列控系统简介 | 第13-14页 |
| 2.2 等级装换场景的描述 | 第14-16页 |
| 2.2.1 CTCS-2 级向CTCS-3 级转换过程 | 第14-16页 |
| 2.2.2 CTCS-3 级向CTCS-2 级转换过程 | 第16页 |
| 2.3 等级转换场景的性能要求 | 第16-17页 |
| 2.4 小结 | 第17-18页 |
| 3 建立UML模型图 | 第18-31页 |
| 3.1 UML概述 | 第18-19页 |
| 3.1.1 UML简介 | 第18-19页 |
| 3.1.2 UML模型的缺点 | 第19页 |
| 3.2 UML顺序图与消息顺序图 | 第19-24页 |
| 3.2.1 C2级向C3级转换的MSC | 第20-23页 |
| 3.2.2 C3级向C2级转换的MSC | 第23-24页 |
| 3.3 UML时序图建模 | 第24-27页 |
| 3.3.1 C2级向C3级转换的UML时序图 | 第25-27页 |
| 3.3.2 C3级向C2级转换的UML时序图 | 第27页 |
| 3.4 UML状态图建模 | 第27-30页 |
| 3.4.1 C2级向C3级转换的状态图 | 第28-29页 |
| 3.4.2 C3级向C2级转换的状态图 | 第29-30页 |
| 3.5 小结 | 第30-31页 |
| 4 UML模型向UPPAAL模型的转换 | 第31-41页 |
| 4.1 时间自动机理论 | 第31-32页 |
| 4.2 验证工具UPPAAL | 第32-33页 |
| 4.2.1 UPPAAL概述 | 第32-33页 |
| 4.2.2 UPPAAL模型元素 | 第33页 |
| 4.3 制定转换规则 | 第33-40页 |
| 4.3.1 MSC向UML时序图模型的转换 | 第33-35页 |
| 4.3.2 UML时序图向UPPAAL模型图的转换 | 第35-36页 |
| 4.3.3 UML状态图向UPPAAL模型图的转换 | 第36页 |
| 4.3.4 UPPAAL模型图添加标志位 | 第36-40页 |
| 4.4 小结 | 第40-41页 |
| 5 模型验证分析 | 第41-50页 |
| 5.1 UPPAAL验证原理 | 第41-44页 |
| 5.1.1 可达性判定 | 第41-42页 |
| 5.1.2 UPPAAL验证语言 | 第42-44页 |
| 5.2 等级转换模型验证 | 第44-49页 |
| 5.2.1 系统性能要求 | 第44-46页 |
| 5.2.2 验证结果分析 | 第46-49页 |
| 5.3 小结 | 第49-50页 |
| 结论 | 第50-51页 |
| 致谢 | 第51-52页 |
| 参考文献 | 第52-55页 |
| 攻读学位期间的研究成果 | 第55页 |
