基于车车通信的列控系统典型运营场景建模与验证

摘要

在CBTC列控系统的基础上，通过车地功能再分配、优化系统结构等形成了基于车车通信的列控系统。该传统具有配置设备少、系统接口和结构简单、维护成本较低等优点。由于列控系统是确保列车实现安全和高效运行的控制系统，如何确保新型的列控系统的功能性、性能性和安全性得到满足显得非常重要。
　　研究的主要内容是基于时间自动机的理论，通过系统建模分析验证工具UPPAAL，对基于车车通信的列控系统典型运营场景进行建模，验证了在该场景下列控系统满足功能性、性能性和安全性的要求。同时利用MATLAB仿真软件对基于移动闭塞制式的折返效率进行仿真验证。主要开展了以下相关工作:
　　(1)对比分析CBTC列控系统和基于车车通信的列控系统的系统架构及控车过程，比较系统架构时以CBTC列控系统作为参考，将比较分为既有功能模块、新增功能模块和相同功能模块转移。比较控车过程时，提出两套系统移动授权生成过程和联锁控制进路存在显著差异。根据比较结果选取移动授权生成场景和折返场景作为列控系统的典型运营场景。
　　(2)明确典型运营场景中包含的对象，如系统的关键设备、彼此交互的信息、实现的流程等。对典型运营场景的术语、功能、通信、环境、特性、属性进行提取。
　　(3)运用时间自动机建模工具通过设置通道、全局变量和函数等，对典型运营场景中各对象进行了模型建立，并构造了时间自动机的积。使用UPPAAL验证工具，结合系统的功能性和实时性需求，以及异常情况下的处理要求对典型运营场景的时间自动机模型进行了分析验证。
　　(4)根据折返时间组成，以及列车运行过程速度变化情况，分别分析基于移动闭塞制式下和基于固定闭塞制式下的折返，通过分段计算时间，得出两种制式下的时间计算方法。最后通过MATLAB仿真折返过程得到仿真曲线，对列车通过道岔速度和折返时间进行仿真，验证了采用基于移动闭塞制式的方式可以有效提高折返效率。

目录

声明

致谢

摘要

1 引言

1．1 选题背景及研究目的和意义

1．2 国内外研究现状

1．3 论文内容及章节安排

1．4 本章小结

2 时间自动机和UPPAAL

2．1 形式化方法基本概念

2．1．1 形式化建模方法

2．1．2 形式化验证方法

2．1．3 时间自动机描述新型列控系统的优势

2．2 时间自动机简介

2．2．2 时间自动机的语义

2．2．3 时间自动机的积

2．3 可达性分析

2．4 模型验证工具UPPAAL

2．5 本章小结

3 基于车车通信列控系统和CBTC列控系统对比分析

3．1 系统框架对比

3．1．1 CBTC列控系统框架

3．1．2 基于车车通信列控系统框架

3．1．3 对比分析

3．2 控车过程对比

3．2．1 CBTC列控系统控车过程

3．2．2 基于车车通信列控系统控车过程

3．2．3 对比分析

3．3 本章小结

4 移动授权生成场景建模与验证

4．1 移动授权生成场景分析

4．1．1 移动授权生成场景流程

4．1．2 移动授权生成场景规范性描述

4．2 移动授权生成场景模型的建立

4．2．1 移动授权生成场景的时序图模型

4．2．2 移动授权生成场景的时间自动机模型

4．3 移动授权生成场景模型验证

4．4 本章小结

5 折返场景建模与验证

5．1 折返场景分析

5．1．1 折返场景流程

5．1．2 折返场景规范性描述

5．1．3 折返效率分析

5．2 折返场景模型的建立

5．2．1 折返场景的时序图模型

5．2．2 折返场景的时间自动机模型

5．3 折返场景模型和效率验证

5．3．1 折返场景模型验证

5．3．2 折返场景效率验证

5．4 本章小结

6 结论

参考文献

图索引

表索引

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

学位论文数据集