A novel framework for supporting the design of moving block train control system schemes

被引:16
作者
Wang, Haifeng [1 ]
Tang, Tao [2 ]
Roberts, Clive [3 ]
Gao, Chunhai [1 ]
Chen, Lei [3 ]
Schmid, Felix [3 ]
机构
[1] Beijing Jiaotong Univ, Natl Engn Res Ctr Rail Transportat Operat & Contr, Beijing 10044, Peoples R China
[2] Beijing Jiaotong Univ, State Key Lab Rail Traff Control & Safety, Beijing 10044, Peoples R China
[3] Univ Birmingham, Birmingham Ctr Railway Res & Educ, Birmingham B15 2TT, W Midlands, England
关键词
Communications-based train control; moving block; formal method; topology; safety-critical software; FORMAL SPECIFICATION;
D O I
10.1177/0954409713495015
中图分类号
TU [建筑科学];
学科分类号
0813 ;
摘要
A moving block philosophy is increasingly being implemented as part of communications-based train control (CBTC) systems in mass transit operations. Due to its complexity and safety criticality, it is difficult to develop formal methods to support the design of specific schemes. An innovative framework, based on topology mathematics, for supporting CBTC moving block system development is proposed in this paper. Within the new framework, the moving block train control logic is transformed into topological spaces representing the movement authority for trains. Using this approach, the verification of logic and safety properties can be performed by automatic assessment of the topological space. Within the paper the essential characteristics of moving block systems, train behaviour and static track-side infrastructure are analysed. As a result of this analysis, topological units are formed to represent train movement trajectory and standard railway network elements. Four calculation methods: dividing, trimming, covering and integrating, are described as standard unit operations. Finally, a case study is implemented to demonstrate how the method is advantageous for CBTC scheme layout development. It is found that the approach is able to bridge the gap between traditional, highly abstracted, formal methods and the specific safety-critical railway scheme designs.
引用
收藏
页码:784 / 793
页数:10
相关论文
共 20 条
[1]  
[Anonymous], 2004, 14741 IVT
[2]  
[Anonymous], 2001, 50128 EN
[3]  
[Anonymous], 2010, Qualification Standard IEC 61508
[4]  
Barger P., 2009, P EUR SAF REL C ESRE, V2, P1303
[5]  
Berkenkötter K, 2004, LECT NOTES COMPUT SC, V3147, P145
[6]   Formal methods: State of the art and future directions [J].
Clarke, EM ;
Wing, JM .
ACM COMPUTING SURVEYS, 1996, 28 (04) :626-643
[7]  
GAAL S., 1964, Point set topology
[8]  
Haifeng Wang, 2010, 2010 2nd International Conference on Industrial Mechatronics and Automation (ICIMA 2010), P453, DOI 10.1109/ICINDMA.2010.5538157
[9]  
Haifeng Wang, 2009, 2009 Asia-Pacific Conference on Computational Intelligence and Industrial Applications (PACIIA 2009), P467, DOI 10.1109/PACIIA.2009.5406388
[10]   A formal approach for the construction and verification of railway control systems [J].
Haxthausen, Anne E. ;
Peleska, Jan ;
Kinder, Sebastian .
FORMAL ASPECTS OF COMPUTING, 2011, 23 (02) :191-219