Formal Techniques for a Data-Driven Certification of Advanced Railway Signalling Systems

  • Alessandro FantechiEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9933)


The technological evolution of railway signalling equipment promises significant increases in transport capacity, in operation regularity, in quality and safety of the service offered.

This evolution is based on the massive use of computer control units on board trains and on the ground, that aims at improving the performance of rail transport and maintaining high safety figures.

A brief review of possible innovation trends of signalling systems shows that they will be more and more based on the exchange of accurate and secure complex information, in order to ensure safe operation.

For this reason we want to advocate the adoption of a novel, data-driven safety certification approach, based on formal verification techniques, focusing on the desired attributes of the exchanged information. A discussion on this issue is presented, based on some initial observations of the needed concepts.


Vital Information Fault Tree Analysis Vital Data Track Circuit Movement Authority 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.



This work is based on an invited presentation made at a workshop funded by the PART project of DTU Compute (Department of Applied Mathematics and Computer Science, Technical University of Denmark), and has been conducted while on leave from University of Florence, thanks to a grant of the Villum Foundation.


  1. 1.
    Bergenhem, C., Pettersson, H., Coelingh, E., Englund, C., Shladover, S., Tsugawa, S.: Overview of platooning systems. In: ITS World Congress, Vienna, 22–26 October 2012Google Scholar
  2. 2.
    Bernardeschi, C., Fantechi, A., Gnesi, S., Larosa, S., Mongardi, G., Romano, D.: A formal verification environment for railway signaling system design. Formal Methods Syst. Des. 12(2), 139–161 (1998)CrossRefGoogle Scholar
  3. 3.
    Biba, K.: Integrity Considerations for Secure Computer Systems. MITRE Co, Bedford (1977)Google Scholar
  4. 4.
    Bock, U., Bikker, G.: Design, development of a future freight train concept- “virtually coupled train formations”. In: Schnieder, E., Becker, U. (eds.): 9th IFAC Symposium Control in Transportation Systems, 13–15 June, S. 410–415, Braunschweig (2000)Google Scholar
  5. 5.
    Bonacchi, A., Fantechi, A., Bacherini, S., Tempestini, M., Cipriani, L.: Validation of railway interlocking systems by formal verification, a case study. In: Counsell, S., Núñez, M. (eds.) SEFM 2013. LNCS, vol. 8368, pp. 237–252. Springer, Heidelberg (2014)CrossRefGoogle Scholar
  6. 6.
    Carnevali, L., Flammini, F., Paolieri, M., Vicario, E.: Non-markovian performability evaluation of ERTMS ETCS level 3. In: Beltrán, M., Knottenbelt, W., Bradley, J. (eds.) EPEW 2015. LNCS, vol. 9272, pp. 47–62. Springer, Heidelberg (2015)CrossRefGoogle Scholar
  7. 7.
    Chandra, T.D., Toueg, S.: Unreliable failure detectors for reliable distributed systems. J. ACM 43(2), 225–267 (1996)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Chen, B., Schmittner, C., Ma, Z., Temple, W.G., Dong, X., Jones, D.L., Sanders, W.H.: Security analysis of urban railway systems: the need for a cyber-physical perspective. In: Koornneef, F., van Gulijk, C. (eds.) SAFECOMP Workshopps 2015. LNCS, vol. 9338, pp. 277–290. Springer, Heidelberg (2015)CrossRefGoogle Scholar
  9. 9.
    Esposito, R., Lazzaro, A., Marmo, P., Sanseviero, A.: Formal verification of ERTMS Euroradio safety critical protocol. In: Proceedings 4th Symposium on Formal Methods for Railway Operation and Control Systems (FORMS 2003). L’Harmattan Hongrie, Budapest (2003)Google Scholar
  10. 10.
    Fantechi, A.: Distributing the challenge of model checking interlocking control tables. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part II. LNCS, vol. 7610, pp. 276–289. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  11. 11.
    Fantechi, A., Gnesi, S., Haxthausen, A., van de Pol, J., Roveri, M., Treharne, H.: SaRDIn - a safe reconfigurable distributed interlocking. In: WCRR 2016, Milano, May 2016Google Scholar
  12. 12.
    Ferrari, A., Magnani, G., Grasso, D., Fantechi, A.: Model checking interlocking control tables. In: Schnieder, E., Tarnai, G. (eds.) FORMS/FORMAT 2010, pp. 107–115. Springer, Heidelberg (2010)Google Scholar
  13. 13.
    Groote, J.F., van Vlijmen, S., Koorn, J.: The safety guaranteeing system at station Hoorn-Kersenboogerd. In: Logic Group Preprint Series 121. Utrecht University (1995)Google Scholar
  14. 14.
    Hase, K.R.: Open proof for railway safety software - a potential way-out of vendor lock-in advancing to standardization, transparency, and software security. In: 8th Symposium on Formal Methods for Automation and Safety in Railway and Automotive Systems (FORMS/FORMAT 2010), 2–3 December 2010, Braunschweig, Germany (2010)Google Scholar
  15. 15.
    Haxthausen, A., Peleska, J.: Formal development and verification of a distributed railway control system. IEEE Trans. Software Eng. 26(8), 687–701 (2000)CrossRefGoogle Scholar
  16. 16.
    Haxthausen, A.E., Peleska, J., Pinger, R.: Applied bounded model checking for interlocking system designs. In: Counsell, S., Núñez, M. (eds.) SEFM 2013. LNCS, vol. 8368, pp. 205–220. Springer, Heidelberg (2014)CrossRefGoogle Scholar
  17. 17.
    Hei, X., Ma, W., Gao, J., Xie, G.: A concurrent scheduling model of distributed train control system. In: IEEE International Conference on Service Operations, Logistics, and Informatics (SOLI), pp. 478–483 (2011)Google Scholar
  18. 18.
    Lamport, L., Shostak, R., Pease, M.: The Byzantine general problem. ACM Trans. Program. Lang. Syst. 4(3), 382–401 (1982)CrossRefzbMATHGoogle Scholar
  19. 19.
    James, P., Lawrence, A., Moller, F., Roggenbach, M., Seisenberger, M., Setzer, A., Kanso, K., Chadwick, S.: Verification of solid state interlocking programs. In: Counsell, S., Núñez, M. (eds.) SEFM 2013. LNCS, vol. 8368, pp. 253–268. Springer, Heidelberg (2014)CrossRefGoogle Scholar
  20. 20.
    James, P., Moller, F., Nguyen, H.N., Roggenbach, M., Schneider, S., Treharne, H., Trumble, M., Williams, D.: Verification of scheme plans using CSP||B. In: Counsell, S., Núñez, M. (eds.) SEFM 2013. LNCS, vol. 8368, pp. 189–204. Springer, Heidelberg (2014)CrossRefGoogle Scholar
  21. 21.
    Kildall, G.A.: A unified approach to global program optimization. In: ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), pp. 194–206 (1973)Google Scholar
  22. 22.
    DaSilva, C., Dehbonei, B., Mejia, F.: Formal specification in the development of industrial applications: subway speed control system. In: Proceedings 5th IFIP Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE 1992), Perros-Guirec, pp. 199–213, North-Holland (1993)Google Scholar
  23. 23.
    Michaut, P.: Method for managing the circulation of vehicles on a railway network and related system. US patent 8820685 B2 (2014)Google Scholar
  24. 24.
    Ohmstede, H.: Method for reducing data in railway operation. US patent 7578485 (2009)Google Scholar
  25. 25.
    de Ruiter, J., Thomas, R.J., Chothia, T.: A formal security analysis of the ERTMS train to trackside protocols. In: Lecomte, T., Pinger, R., Romanovsky, A. (eds.) RSSRail 2016. LNCS, vol. 9707, pp. 53–68. Springer, Heidelberg (2016)CrossRefGoogle Scholar
  26. 26.
    Sanders, W.H.: Quantitative security metrics: unattainable holy grail or a vital breakthrough within our reach? IEEE Secur. Priv. 12(2), 67–69 (2014)CrossRefGoogle Scholar
  27. 27.
    Schulz, O., Peleska, J.: Reliability analysis of safety-related communication architectures. In: Schoitsch, E. (ed.) SAFECOMP 2010. LNCS, vol. 6351, pp. 1–14. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  28. 28.
    Totel, E., Blanquart, J.-P., Deswarte, Y., Powell, D.: Supporting multiple levels of criticality, digest of papers. In: FTCS-28, The Twenty Eigth Annual International Symposium on Fault-Tolerant Computing, Munich, Germany, 23–25 June 1998, pp. 70–79. IEEE Computer Society (1998)Google Scholar
  29. 29.
  30. 30.
    Weiser, M.: Program slicing. IEEE Trans. Software Eng. 10(4), 352–357 (1984)CrossRefzbMATHGoogle Scholar
  31. 31.
    Whitwam, F., Kanner, A.: Control of automatic guided vehicles without wayside interlocking. US patent 20120323411 A1 (2012)Google Scholar
  32. 32.
    Winter, K., Robinson, N.J.: Modelling large railway interlockings and model checking small ones. In: Twenty-Sixth Australasian Computer Science Conference (ACSC 2003), pp. 309–316 (2003)Google Scholar
  33. 33.
    Zimmermann, A., Hommel, G.: Towards modeling and evaluation of ETCS real-time communication and operation. J. Syst. Softw. 77(1), 47–54 (2005)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG 2016

Authors and Affiliations

  1. 1.DTU ComputeLyngbyDenmark
  2. 2.University of Florence - DINFOFlorenceItaly

Personalised recommendations