Abstract
ERTMS/ETCS is a European signalling, control and train protection system. In this paper, we model and analyse this complex system of systems, including its hybrid elements, on the design level in Real-Time Maude. Our modelling allows us to formulate safety properties in physical rather than in logical terms. We systematically validate our model by simulation and error injection. Using the Real-Time Maude model-checker, we effectively verify a number of small rail systems.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
We focus here on one ERTMS/ETCS system controlling a single, geographic region.
- 2.
It is a design decision whether a topological route appears in the control table. The routes in the table are those available for use by trains.
- 3.
At this point, there should be maximally one route available that matches a particular train. This is ensured by the requests from the controller and also the ability of the interlocking to deny requests for conflicting routes.
- 4.
The models are available at: http://www.cs.swan.ac.uk/%7Ecsmarkus/ProcessesAndData/Models.
- 5.
Compared to the given control table, we add RouteName4 to cover the exit track.
- 6.
Using a PC running Xubuntu 14.04.2 with an i7 4790 @3.60Â Ghz and 32Â GB RAM.
References
openETCS (2015). http://openetcs.org. Accessed 30 August 2015
Alcatel, Alstom, Ansaldo Signal, Bombardier, Invensys Rail and Siemens. System Requirements Specification, Chap. 2, Basic System Description (2006). SUBSET-026-2
Chiappini, A., Cimatti, A., Macchi, L., Rebollo, O., Roveri, M., Susi, A., Tonetta, S., Vittorini, B.: Formalization and validation of a subset of the european train control system. In: Proceedings of ICSE 2010. ACM Press (2010)
Rizzo, T., Sanseviero, A., Roveri, M., Narasamdya, I., Tchaltsev, A., Lazzaro, A., Corvino, R., Cimatti, A.: Formal verification and validation of ERTMS industrial railway train spacing system. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 378–393. Springer, Heidelberg (2012)
Clavel, M., Durán, F., Eker, S., Lincoln, P., MartÃ-Oliet, N., Meseguer, J., Talcott, C.L. (eds.): All About Maude. LNCS, vol. 4350. Springer, Heidelberg (2007)
Eker, S., Meseguer, J., Sridharanarayanan, A.: The Maude LTL model checker. In: WRLA 2002, vol. 71, ENTCS. Elsevier (2002)
European Railway Industry. ERTMS (2015). http://www.era.europa.eu/Core-Activities/ERTMS/Pages/home.aspx. Accessed 30 August 2015
Henzinger, T.A.: The theory of hybrid automata. In: Inan, M.K., Kurshan, R.P. (eds.) Verification of Digital and Hybrid Systems. NATO ASI Series, vol. 170, pp. 265–292. Springer, Heidelberg (2000)
James, P., Moller, F., Nga, N.H., Roggenbach, M., Schneider, S.A., Treharne, H.: Techniques for modelling and verifying railway interlockings. STTT 16(6), 685–711 (2014)
James, P., Moller, F., Nguyen, H.N., Roggenbach, M., Schneider, S.A., Treharne, H.: On modelling and verifying railway interlockings: tracking train lengths. Sci. Comput. Program. 96, 315–336 (2014)
James, P., Roggenbach, M.: Encapsulating formal methods within domainspecific languages: a solution for verifying railway scheme plans. Math. Comput. Sci. 8(1), 11–38 (2014)
Lawrence, A., Berger, U., James, P., Roggenbach, M., Seisenberger, M.: Modelling and analysing the european rail traffic management system in Real-Time Maude. In: FTSCS 2014 - Preliminary Proceedings (2014)
Meseguer, J., Ölveczky, P.C.: Semantics and pragmatics of Real-Time Maude. Higher-Order Symbolic Comput. 20(1–2), 161–196 (2007)
Nardone, R., Gentile, U., Peron, A., Benerecetti, M., Vittorini, V., Marrone, S., De Guglielmo, R., Mazzocca, N., Velardi, L.: Dynamic state machines for formalizing railway control system specifications. In: Artho, C., Ölveczky, P.C. (eds.) FTSCS 2014. CCIS, vol. 476, pp. 93–109. Springer, Heidelberg (2015)
Ölveczky, P.C., Meseguer, J.: Abstraction and completeness for Real-Time Maude. In: WRLA 2006, vol. 176, ENTCS (2007)
Meseguer, J., Ölveczky, P.C.: The Real-Time Maude tool. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 332–336. Springer, Heidelberg (2008)
Thorvaldsen, S., Ölveczky, P.C.: Formal modeling and analysis of the OGDC wireless sensor network algorithm in Real-Time Maude. In: Bonsangue, M.M., Johnsen, E.B. (eds.) FMOODS 2007. LNCS, vol. 4468, pp. 122–140. Springer, Heidelberg (2007)
Vu, L.H., Haxthausen, A.E., Peleska, J.: Formal modeling and verification of interlocking systems featuring sequential release. In: Artho, C., Ölveczky, P.C. (eds.) FTSCS 2014. CCIS, vol. 476, pp. 223–238. Springer, Heidelberg (2015)
Acknowledgement
The authors would like to thank Simon Chadwick, Siemens Rail Automation, UK, for his continued support and many helpful discussions. We also appreciate the helpful advice from Peter Ölveczky on Real-Time Maude and the constructive comments given by three anonymous referees. Finally, we thank Erwin R. Catesbeiana (Jr.) for timely hints on how to stay on track.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
James, P., Lawrence, A., Roggenbach, M., Seisenberger, M. (2016). Towards Safety Analysis of ERTMS/ETCS Level 2 in Real-Time Maude. In: Artho, C., Ölveczky, P. (eds) Formal Techniques for Safety-Critical Systems. FTSCS 2015. Communications in Computer and Information Science, vol 596. Springer, Cham. https://doi.org/10.1007/978-3-319-29510-7_6
Download citation
DOI: https://doi.org/10.1007/978-3-319-29510-7_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-29509-1
Online ISBN: 978-3-319-29510-7
eBook Packages: Computer ScienceComputer Science (R0)