基于COMET的西部铁路列控系统RBC信息控制流程设计与验证

摘要

随着“一带一路”战略的推进以及我国中东部地区铁路网的不断完善，西部地区将迎来铁路发展的黄金时期。CTCS-LDL（Chinese Train Control System-LowDensity Lines）级列控系统是针对我国西部地区低密度线路运营需求而研发的新型列控系统，目前该系统处于理论探索阶段。为降低运营成本，减少或免于地面设备维护，CTCS-LDL级列控系统使用GNSS技术实现列车定位及完整性检查，地面不设区间轨道电路和信号机，采用虚拟闭塞方式实现列车追踪，这样对地面设备的安全性和可靠性提出了更高的要求。无线闭塞中心(RBC)是CTCS-LDL级列控系统的地面核心设备，主要通过与车载及地面其他设备间的信息交互，实现虚拟轨道占用检查与区间闭塞管理，完成行车控制，因此设计合理的RBC信息控制流程是保证西部铁路列控系统安全行车的基础。
　　通过分析我国低密度线路列控系统的运营需求，本论文将RBC信息控制流程分为地面信息控制流程与控车流程，对其进行设计、建模与验证。论文完成的主要工作如下:
　　首先，通过比较基于UML的COMET(Collaborative Object Modeling andArchitectural Design Method)建模方法与基于时间自动机理论的形式化建模方法的优缺点，将二者结合，提出针对RBC的COMET软件建模与验证方法，该方法涵盖了软件开发周期中需求分析、软件建模、模型验证、架构设计、软件编码这一集成化过程。
　　然后，对RBC系统进行功能需求分析，设计系统总体结构模型，将RBC信息控制流程分为地面信息控制流程和控车流程。地面信息控制流程包括轨道占用识别、区间信号点灯和区间改方;控车流程根据运行场景主要分为设备启动、列车注册、正常行车、列车注销、调车、RBC切换等。对上述流程进行详细设计，并建立COMET动态交互模型，再通过转换算法将其转换为时间自动机网络模型。结合RBC系统的功能需求，利用模型验证工具UPPAAL对建立的模型进行仿真，并从逻辑功能、时序功能和安全性的角度对模型进行分析验证。
　　最后，根据建立的RBC信息控制模型，采用COMET分层抽象的软件体系架构，进行仿真软件设计并完成软件开发。通过实验室仿真联调，验证了本文设计的CTCS-LDL级列控系统中RBC信息控制流程的正确性和合理性。

目录

声明

致谢

摘要

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 展望

参考文献

图索引

表索引

作者简历及攻读硕士学位期间取得的研究成果

学位论文数据集