基于UPPAAL的系统建模验证研究及其在CTCS-3列控系统的应用
| 致谢 | 第1-6页 |
| 中文摘要 | 第6-7页 |
| ABSTRACT | 第7-11页 |
| 1 引言 | 第11-18页 |
| ·研究背景及意义 | 第11-12页 |
| ·国内外研究现状 | 第12-13页 |
| ·列控系统建模验证 | 第12-13页 |
| ·形式化方法建模验证 | 第13页 |
| ·CTCS-3级列控系统简介 | 第13-14页 |
| ·本文研究内容及组织结构 | 第14-18页 |
| ·研究内容 | 第15-16页 |
| ·文章的组织结构 | 第16-18页 |
| 2 RBC切换场景UML建模 | 第18-39页 |
| ·场景描述 | 第18-20页 |
| ·概述 | 第18-19页 |
| ·RBC切换原则 | 第19-20页 |
| ·统一建模语言UML及扩展 | 第20-24页 |
| ·UML简介 | 第20-22页 |
| ·UML顺序图 | 第22-23页 |
| ·顺序图扩展 | 第23-24页 |
| ·建立UML模型 | 第24-39页 |
| ·建立UML类图 | 第25-27页 |
| ·建立UML顺序子图 | 第27-36页 |
| ·建立UML顺序图及扩展 | 第36-39页 |
| 3 UML模型转UPPAAL模型 | 第39-61页 |
| ·时间自动机 | 第39-42页 |
| ·自动机概述 | 第39页 |
| ·时间自动机 | 第39-42页 |
| ·模型分析验证工具UPPAAL | 第42-44页 |
| ·UPPAAL结构 | 第42-43页 |
| ·UPPAAL理论模型 | 第43-44页 |
| ·UML顺序图的时间自动机构造 | 第44-49页 |
| ·UML顺序图的对象自动机构造 | 第44-49页 |
| ·抽取顺序图时间约束构造模型 | 第49页 |
| ·UPPAA模型 | 第49-61页 |
| ·UPPAAL子模型 | 第50-56页 |
| ·UPPAAL整体模型 | 第56-61页 |
| 4 基于UPPAAL的RBC切换验证分析 | 第61-71页 |
| ·组建时间自动机网络 | 第61-62页 |
| ·建立时间自动机网络 | 第61-62页 |
| ·基于时间自动机网络的形式化验证方法 | 第62页 |
| ·RBC切换的模拟仿真 | 第62-66页 |
| ·处理模块的模拟仿真 | 第63-66页 |
| ·RBC切换验证分析 | 第66-71页 |
| 5 结论与展望 | 第71-73页 |
| ·论文总结 | 第71-72页 |
| ·展望 | 第72-73页 |
| 参考文献 | 第73-76页 |
| 附录A | 第76-79页 |
| 图索引 | 第79-81页 |
| 表索引 | 第81-82页 |
| 作者简历 | 第82-84页 |
| 学位论文数据集 | 第84页 |
