基于时间自动机的RBC控车流程研究
| 摘要 | 第1-7页 |
| Abstract | 第7-11页 |
| 第1章 绪论 | 第11-16页 |
| ·研究背景 | 第11-13页 |
| ·欧洲列车控制系统现状 | 第11-12页 |
| ·中国列车控制系统现状 | 第12-13页 |
| ·CTCS-3级RBC控车系统建模的目的和意义 | 第13-14页 |
| ·论文的主要工作和章节安排 | 第14-16页 |
| 第2章 形式化描述方法 | 第16-27页 |
| ·形式化方法 | 第16-19页 |
| ·形式化方法概述 | 第16-17页 |
| ·形式化方法选择 | 第17-18页 |
| ·形式化模型验证 | 第18页 |
| ·形式化建模优点 | 第18-19页 |
| ·时间自动机 | 第19-27页 |
| ·自动机概述 | 第19-20页 |
| ·时间自动机 | 第20-23页 |
| ·时间自动机简例 | 第23-24页 |
| ·时间自动机可达性分析 | 第24-25页 |
| ·时间自动机优点 | 第25-27页 |
| 第3章 RBC控车流程分析与设计 | 第27-45页 |
| ·CTCS-3级列控RBC系统介绍 | 第27-31页 |
| ·CTCS-3级列控系统 | 第27-28页 |
| ·地面RBC子系统 | 第28-31页 |
| ·RBC子系统功能需求分析 | 第31-33页 |
| ·RBC系统控车流程分析与设计 | 第33-45页 |
| ·消息重新发送流程 | 第35-37页 |
| ·列车登陆流程 | 第37-38页 |
| ·正常控车流程 | 第38-40页 |
| ·RBC移交流程 | 第40-43页 |
| ·列车注销流程 | 第43-45页 |
| 第4章 基于UPPAAL的RBC控车流程建模 | 第45-64页 |
| ·时间自动机建模工具UPPAALL介绍 | 第45-50页 |
| ·UPPAAL结构简介 | 第46-47页 |
| ·UPPAAL理论模型 | 第47-50页 |
| ·RBC控车流程建模 | 第50-60页 |
| ·消息重发模型 | 第50-52页 |
| ·列车登陆模型 | 第52-54页 |
| ·正常控车模型 | 第54-56页 |
| ·RBC移交模型 | 第56-59页 |
| ·列车注销模型 | 第59-60页 |
| ·其他子系统简单建模 | 第60-64页 |
| ·车载模块简单模型 | 第60-62页 |
| ·地面其他模块简单模型 | 第62-64页 |
| 第5章 RBC控车模型功能验证 | 第64-75页 |
| ·在UPPAAL中构造时间自动机的积 | 第64-65页 |
| ·消息重发流程系统模型验证 | 第65-68页 |
| ·模型仿真 | 第65-66页 |
| ·模型仿真结果验证 | 第66-68页 |
| ·RBC控车系统流程模型验证 | 第68-75页 |
| ·模型仿真 | 第68-72页 |
| ·模型仿真结果验证 | 第72-75页 |
| 结论 | 第75-76页 |
| 致谢 | 第76-77页 |
| 参考文献 | 第77-80页 |
| 攻读硕士学期间发表的学术论文及科学实践 | 第80页 |
