基于UPPAAL的RBC系统控车流程建模分析
| 致谢 | 第1-6页 |
| 中文摘要 | 第6-7页 |
| ABSTRACT | 第7-10页 |
| 1 引言 | 第10-16页 |
| ·列控系统发展现状 | 第10-13页 |
| ·国外列控系统现状 | 第11-12页 |
| ·国内列控系统现状 | 第12-13页 |
| ·论文研究的目的和意义 | 第13-14页 |
| ·论文章节安排 | 第14-16页 |
| 2 分析工具UPRAAL介绍 | 第16-28页 |
| ·形式化方法 | 第16-18页 |
| ·形式化方法概述 | 第16-17页 |
| ·形式化方法分类 | 第17-18页 |
| ·形式化方法优点 | 第18页 |
| ·时间自动机 | 第18-23页 |
| ·自动机概述 | 第18-19页 |
| ·时间自动机 | 第19-22页 |
| ·可达性分析 | 第22页 |
| ·时间自动机优点 | 第22-23页 |
| ·模型分析验证工具UPPAAL | 第23-28页 |
| ·UPPAAL结构 | 第23-25页 |
| ·UPPAAL理论模型 | 第25-28页 |
| 3 RBC系统控车流程分析与设计 | 第28-42页 |
| ·RBC系统介绍 | 第28-31页 |
| ·CTCS-3级系统 | 第28-29页 |
| ·RBC子系统 | 第29-31页 |
| ·RBC系统控车流程分析设计 | 第31-41页 |
| ·列车登录流程 | 第33-34页 |
| ·正常控车流程 | 第34-37页 |
| ·RBC交接流程 | 第37-38页 |
| ·列车注销流程 | 第38-39页 |
| ·消息重发流程 | 第39-41页 |
| ·系统需求 | 第41-42页 |
| 4 基于时间自动机的RBC控车流程建模 | 第42-55页 |
| ·RBC控车流程建模 | 第42-50页 |
| ·列车登录模型 | 第42-44页 |
| ·正常控车模型 | 第44-46页 |
| ·RBC交接模型 | 第46-47页 |
| ·列车注销模型 | 第47-48页 |
| ·消息重发模型 | 第48-50页 |
| ·外部设备建模 | 第50-55页 |
| ·列车模型 | 第50-53页 |
| ·其他地面设备模型 | 第53-55页 |
| 5 基于UPPAAL的RBC控车流程验证分析 | 第55-65页 |
| ·构造时间自动机的积 | 第55-56页 |
| ·使用UPRAAL构造时间自动机的积 | 第55-56页 |
| ·RBC消息重发流程分析验证 | 第56-59页 |
| ·消息重发流程仿真分析 | 第56-58页 |
| ·消息重发流程验证 | 第58-59页 |
| ·RBC控车流程分析验证 | 第59-65页 |
| ·RBC控车流程仿真分析 | 第59-63页 |
| ·RBC控车流程验证 | 第63-65页 |
| 6 结论与展望 | 第65-66页 |
| ·结论 | 第65页 |
| ·展望 | 第65-66页 |
| 参考文献 | 第66-68页 |
| 作者简历 | 第68-70页 |
| 学位论文数据集 | 第70页 |
