摘要:CBTC(Communication Based Train Control)系统是轨道交通的一种新兴的系统,该系统能够很好的提高城市轨道交通中的列车运行效率,也能减少系统在建设和文护方面的不必要费用。为了保证该系统在运营过程中的安全性,在对该系统的研究过程中需要对其进行仿真、建模及验证,从而找到该系统的设计缺陷。CBTC系统中区域控制子系统是一个实时的控制系统,它不仅需要对时间控制得精确还要对过程控制得准确。本课题通过对CBTC区域控制器的结构进行分析从而给出满足该子系统安全的功能、性能的要求,同时结合时间自动机理论做出包括列车、时间速度控制器、区域控制器和多列车队列的时间自动网络模型结构。该结构应用UPPAAL,验证工具来对此子系统进行仿真,验证其功能和性能的要求,以此保证模型的安全性和受限性。
关键词:CBTC区域控制器;UPPAAL;时间自动机
CBTC in Zone Control Subsystem of Urban Rail Transit Formal Modeling and Verification
Abstract: CBTC (Communication Based Train Control) is a good system of rail transit. it can effectively improve the efficiency of rail transit train running and reducing the cost of system in the construction and maintenance. In order to ensure the safety in the process of the system in operation, the simulation, modeling and verification method is needed in the study of the system to find design defect of the system. CBTC in ZC subsystem is a real-time control system, it needs not only to time control precision but accurate for process control. This paper analysis the structure of area of CBTC controller so as to meet the requirements of function, performance of the security subsystem. A time automata model is designed to simulate the process of CBTC control system based on UPPAAL. The model consists of trains, speed and distance control, ZC Control and the queue modules. The simulation results verify its functionality and performance requirements and assure the security and the limited of the model.
Key Words:Zone Control Subsystem of CBTC; UPPAAL; timed automata
目录
1 绪论 1
1.1 课题的目的和意义 1
1.2 国内外研究现状与水平 1
1.3 发展趋势 2
2 CBTC系统 3
2.1 CBTC系统的概况及原理 3
2.1.1 简述CBTC系统 3
2.1.2 CBTC系统原理 4
2.2 CBTC系统中ZC子系统 5
2.2.1 ZC子系统的组成 6
2.2.2 ZC子系统的工作原理 7
3 CBTC区域控制器的时间自动机模型与仿真 10
3.1 模型结构设计 10
3.1.1 列车模块 11
3.1.2 速度-距离控制器模块 13
3.1.3 ZC控制器模块 15
3.1.4 多列车控制队列模块 16
3.2 模型的仿真与验证 18
3.2.1运行调试结果 18
3.2.2调试结果分析 20
4 结论 23
致谢 24
参考文献 25
1 绪论
1.1 课题的目的和意义
基于通信的列车控制系统CBTC (Communication Based Train Control) 是不依赖轨道电路的一个列车控制系统,它采用了高精度的列车定位系统和连续、高速、双向车-地数据的通信技术,是通过车载系统和地面安全设备实现对列车控制的列车控制系统。列车能够以较小的间隔距离运行,这样就可以实现“小编组、高密度”的这种运营模式,这就使得系统能在保证了客运需求的基础上,缩短乘客候车时间,站台的长度和候车空间等因素,同时降低了基建投资[1]。 城市轨道交通CBTC区域控制形式化建模与验证:http://www.youerw.com/zidonghua/lunwen_11451.html