Novel Online Safety Observer for Railway Interlocking System
Publication: Journal of Transportation Engineering
Volume 139, Issue 7
Abstract
Due to the complexity and size of railway interlocking systems, conventional verification and testing techniques are not able to provide sufficient safety assurance. This paper proposes an online observer for safety assurance of railway interlocking systems. The observer provides runtime checking of the states and behaviors of interlocking devices by using a topology-based mathematical model. Route signals, points, and track sections are interpreted in a topological space, and safety properties are expressed as topology theorems. Running synchronously with the interlocking task, the observer conducts safety checks on the route processes and point operations. A case study of an example Chinese railway interlocking system is presented to illustrate the proposed method and its strengths. It is anticipated that this method will provide a fresh means to verify safety properties of railway interlocking systems in addition to traditional testing and verification methods.
Get full access to this article
View all available purchase options and get full access to this article.
Acknowledgments
This work was supported in part by the National 863 plans projects under Grant 2011AA010104 and the State Key Laboratory of Rail Traffic Control and Safety under Grant RCS2011ZZ001, P.R. China. The authors wish to convey sincere appreciation to Mr. James Mistry from BT for his time to proofread this paper.
References
Antoni, M., and Ammad, N. (2008). “Formal validation method and tools for French computerized railway interlocking systems.” Proc., Railway Condition Monitoring, 2008 4th IET Int. Conf., The Institution of Engineering and Technology, London, 1–10.
Barger, P., Schoen, W., and Bouali, M. (2009). “A study of railway ERTMS safety with colored Petri nets.” Proc., European Safety and Reliability Conf., CRC Press-Taylor & Francis Group, Boca Raton, FL, 1303–1309.
Basile, F., Chiacchio, P., and De Tommasi, G. (2009). “An efficient approach for online diagnosis of discrete event systems.” IEEE Trans. Autom. Control, 54(4), 748–759.
Bernardeschi, C., Fantechi, A., Gnesi, S., Larosa, S., Mongardi, G., and Romano, D. (1998). “A formal verification environment for railway signaling system design.” Form. Methods Syst. Des., 12(2), 139–161.
Calame, J. R., Goga, N., Ioustinova, N., and Pol, J. v. d. (2006). “TTCN-3 testing of Hoorn-Kersenboogerd railway interlocking.” Proc., Electrical and Computer Engineering, 2006, IEEE, New York, 620–623.
Cimatti, A., Giunchiglia, F., Mongardi, G., Romano, D., Torielli, F., and Traverso, P. (1998). “Model checking safety critical software with SPIN: An application to a railway interlocking system.” Proc., Computer Safety, Reliability and Security, Springer-Verlag, London, UK, 284–295.
Clarke, E. M., and Wing, J. M. (1996). “Formal methods: State of the art and future directions.” Acm Computing Surveys, 28(4), 626–643.
Diaz, M., Juanole, G., and Courtiat, J. P. (1994). “Observer-a concept for formal on-line validation of distributed systems.” IEEE Trans. Software Eng., 20(12), 900–913.
European Committee for Electrotechnical Standardization (CENELEC). (2001). “Railway applications—Communications, signalling and processing systems—Software for railway control and protection systems.”, Brussels, Belgium.
Gaal, S. A. (1964). Point set topology, Academic, New York.
Guo, J., Zhu, C. Q., and Yang, Y. (2003). “Performance evaluation of railway computer interlocking system based on queuing theory.” Proc., Parallel and Distributed Computing, Applications and Technologies, 2003, IEEE, New York, 420–423.
Hartonas-Garmhausen, V., Campos, S., Cimatti, A., Clarke, E., and Giunchiglia, F. (2000). “Verification of a safety-critical railway interlocking system with real-time constraints.” Sci. Comput. Program., 36(1), 53–64.
Haxthausen, A., Kjær, A., and Bliguet, M. (2011a). “Formal development of a tool for automated modelling and verification of relay interlocking systems.” Proc., FM 2011: Formal Methods, Springer, Berlin, 118–132.
Haxthausen, A. E., Peleska, J., and Kinder, S. (2011b). “A formal approach for the construction and verification of railway control systems.” Formal Aspect. Comput., 23(2), 191–219.
He, W. (1997). 6502 electric circuit of railway interlocking, China Railway, Beijing.
Jo, H.-J., Yoon, Y.-K., and Hwang, J.-G. (2009). “Analysis of the formal specification application for train control systems.” J. Electr. Eng. Technol., 4(1), 87–92.
Kanso, K., Moller, F., and Setzer, A. (2009). “Automated verification of signalling principles in railway interlocking systems.” Electron. Notes Theor. Comput. Sci., 250(2), 19–31.
Kinnersley, S., and Roelen, A. (2007). “The contribution of design to accidents.” Saf. Sci., 45(1–2), 31–60.
Kollmann, M., and Hon, Y. M. (2007). “Generating scenarios by multi-object checking.” Electron. Notes Theor. Comput. Sci., 190(2), 61–72.
Kyriakidis, M., Hirsch, R., and Majumdar, A. (2012). “Metro railway safety: An analysis of accident precursors.” Saf. Sci., 50(7), 1535–1548.
Leucker, M., and Schallhart, C. (2009). “A brief account of runtime verification.” J. Logic Algebr. Program., 78(5), 293–303.
Padberg, J., Jansen, L., Ehrig, H., Schnieder, E., and Heckel, R. (2001). “Cooperability in train control systems: Specification of scenarios using open nets.” J. Integr. Des. Process Sci., 5(1), 3–21.
Ramirez-Trevino, A., Ruiz-Beltran, E., Rivera-Rangel, I., and Lopez-Mellado, E. (2007). “Online fault diagnosis of discrete event systems. A Petri net-based approach.” IEEE Trans. Autom. Sci. Eng., 4(1), 31–39.
Roanes-Lozano, E., Hernando, A., Alonso, J. A., and Laita, L. M. (2011). “A logic approach to decision taking in a railway interlocking system using Maple.” Math. Comput. Simul., 82(1), 15–28.
Theeg, G., and Vlasenko, S. (2009). Railway signalling & interlocking, Eurailpress, Hamburg, Germany.
Wang, H.-f., and Li, W. (2008). “Component-based safety computer of railway signal interlocking system.” Proc., Computing, Communication, Control, and Management, 2008, IEEE Computer Society, Los Alamitos, CA, 538–541.
Wang, H.-F., and Liu, S. (2010). “Modeling communications-based train control system: A case study.” Proc., 2nd Int. Conf. on Industrial Mechatronics and Automation, IEEE, New York, 453–456.
Wang, H.-F., Liu, S., and Gao, C. (2009). “Study on model-based safety verification of automatic train protection system.” Proc., Asia-Pacific Conf. on Computational Intelligence and Industrial Applications, IEEE, New York, 467–470.
Woodcock, J., Larsen, P. G., Bicarregui, J., and Fitzgerald, J. (2009). “Formal methods: Practice and experience.” ACM Comput. Surv., 41(4), 1–36.
Zafar, N. A. (2009). “Formal specification and validation of railway network components using Z notation.” IET Software, 3(4), 312–320.
Zhao, Y., Oberthür, S., Kardos, M., and Rammig, F. J. (2006). “Model-based runtime verification framework for self-optimizing systems.” Electron. Notes Theor. Comput. Sci., 144(4), 125–145.
Zimmermann, A., and Hommel, G. (2005). “Towards modeling and evaluation of ETCS real-time communication and operation.” J. Syst. Softw., 77(1), 47–54.
Information & Authors
Information
Published In
Journal of Transportation Engineering
Volume 139 • Issue 7 • July 2013
Pages: 719 - 727
Copyright
© 2013 American Society of Civil Engineers.
History
Received: Nov 1, 2012
Accepted: Feb 25, 2013
Published online: Feb 27, 2013
Published in print: Jul 1, 2013
Authors
Metrics & Citations
Metrics
Citations
Download citation
If you have the appropriate software installed, you can download article citation data to the citation manager of your choice. Simply select your manager software from the list below and click Download.