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

Abstract

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.

Keywords

Communications-based train control moving block formal method topology safety-critical software

Get full access to this article

View all access options for this article.

References

Wang

Zhang

Theoretical analysis of block carrying capacity under moving autoblock system. In: Mellitt

Hill

Allan

(eds). Computers in railways VI, Southampton, UK: Computational Mechanics Publications Ltd, 1998, pp. 981–990.

Lockyear MJ. The application of a transmission based moving block automatic train control system on Docklands Light Railway. In: The international conference on developments in mass transit systems, London, UK, 20–23 April 1998, pp. 51–61.

Ning

Absolute braking and relative distance braking - train operation control modes in moving block systems. In: Mellitt

Hill

Allan

(eds). Computers in railways VI, Southampton: Computational Mechanics Publications Ltd, 1998, pp. 991–1001.

Morar S. Evolution of communication based train control worldwide. In: The IET professional development course on railway signalling and control systems, London, UK, 21–24 May 2012, pp. 218–226. Stevenage, UK: IET Press.

Woodcock

Larsen

Bicarregui

Fitzgerald

. Formal methods: practice and experience. ACM Comput Surv 2009; 41(4): 1–36.

Clarke

Wing

. Formal methods: state of the art and future directions. ACM Comput Surv 1996; 28(4): 626–643.

Zafar

. Formal specification and validation of railway network components using Z notation. IET Softw 2009; 3(4): 312–320.

H-J

Yoon

Y-K

Hwang

J-G

. Analysis of the formal specification application for train control systems. J Electr Engng Technol 2009; 4(1): 87–92.

Haxthausen

Peleska

Kinder

. A formal approach for the construction and verification of railway control systems. Form Asp Comput 2011; 23(2): 191–219.

10.

IEC 61508: 2010. Functional safety of electrical/electronic/programmable electronic systems.

11.

EN 50128: 2001. Railway applications –communications, signalling and processing systems – software for railway control and protection systems.

12.

Zimmermann

Hommel

. Towards modeling and evaluation of ETCS real-time communication and operation. J Syst Softw 2005; 77(1): 47–54.

13.

Padberg

Jansen

Ehrig

. Cooperability in train control systems: specification of scenarios using open nets. J Integr Des Process Sci 2001; 5(1): 3–21.

14.

Barger P, Schoen W and Bouali M. A study of railway ERTMS safety with colored Petri nets. In: Soares CG, Martorell S and Bris R (eds) European safety and reliability conference, Prague, Czech Republic, 7–10 September 2009, pp. 1303–1309. Prague, CRC Press.

15.

Wang H and Liu S. Study on model-based safety verification of automatic train protection system. In: The IEEE Asia-Pacific conference on computational intelligence and industrial applications, Wuhan, China, 29 November 2009, pp. 467–470. Piscataway, NJ: IEEE Press.

16.

Wang H and Liu S. Modeling communications-based train control system: a case study. In: Luo Q (ed) The second IEEE international conference on industrial mechatronics and automation, Wuhan, China, 30–31 May 2010, pp. 453–456. Piscataway, NJ: IEEE Press.

17.

Berkenkotter

Bisanz

Hannemann

Peleska

. Executable hybrid UML and its application to train control systems. In: Ehrig H, Damm W, Große-Rhode M, Reif W, Schnieder E and Westkämper (eds) Integration of software specification techniques for applications in engineering, Berlin, Germany: Springer-Verlag, 2004, pp. 145–173.

18.

Parnas

. Really rethinking ‘formal methods'. Computer 2010; 43(1): 28–34.

19.

IEEE IVT 1474.1: 2004. IEEE standard for communications-based train control (CBTC) performance and functional requirements.

20.

Gaal

. Point set topology, New York, NY: Academic Press, 1964.