声明
致谢
摘要
1.1 研究背景
1.2 国内外研究现状
1.2.1 低密度线路列控系统研究现状
1.2.2 列控系统建模研究现状
1.3 CTCS-LDL级列控系统概述
1.4 论文研究目的及意义
1.5 论文的研究内容及结构
2 COMET软件建模及其形式化验证方法研究
2.1 COMET软件建模与设计方法
2.1.1 COMET软件建模与设计方法
2.1.2 COMET动态交互建模
2.2 时间自动机理论
2.2.1 时间自动机
2.2.2 形式化验证工具UPPAAL
2.3 COMET-TA模型转换算法
2.3.1 状态相关的UML顺序图
2.3.2 UML顺序图-TA模型转换
2.3.3 UML活动图-TA模型转换
2.4 针对RBC的COMET建模与验证方法
2.5 本章小结
3 西部铁路列控系统RBC功能需求分析
3.1 RBC系统功能分析
3.1.1 RBC系统功能分析
3.1.2 RBC系统外部交互设备
3.2 RBC功能需求建模
3.2.1 RBC系统用例建模
3.2.2 RBC数据流分析
3.3 本章小结
4 地面信息控制流程设计与形式化验证
4.1 虚拟闭塞控制与信号点灯
4.2 轨道区段占用识别
4.2.1 列车位置分析
4.2.2 虚拟轨道区段占用状态分析
4.2.3 区间轨道区段占用识别
4.2.4 站内轨道区段占用识别
4.3 区间运行方向控制
4.3.1 RBC控制区域内区间改方
4.3.2 RBC交接区域区间改方
4.4 基于UPPAAL的地面信息控制模型
4.4.1 轨道占用与信号点灯模型
4.4.2 区间改方模型
4.5 模型仿真与验证
4.5.1 UPPAAL模拟仿真
4.5.2 模型验证
4.6 本章小结
5 控车流程设计与形式化验证
5.1 低密度线路RBC控车特点分析
5.2 控车流程分析设计
5.2.1 设备启动
5.2.2 列车注册
5.2.3 正常行车
5.2.4 调车
5.2.5 列车注销
5.2.5 RBC切换
5.3 基于UPPAAL的RBC控车模型
5.3.1 RBC控车场景关系
5.3.2 控车流程的时间自动机网络构建
5.3.3 常规场景下RBC控车模型
5.3.4 RBC切换场景下的控车模型
5.4 模型验证
5.4.1 逻辑功能验证
5.4.2 时序功能验证
5.4.3 安全性验证
5.5 本章小结
6 RBC仿真软件设计与实现
6.1 软件架构设计
6.2 功能实现与相关界面
6.3 联调及仿真结果
6.4 小结
7.1 总结
7.2 展望
参考文献
图索引
表索引
作者简历及攻读硕士学位期间取得的研究成果
学位论文数据集