Skip to main content
SpringerLink
Log in

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

  • Conference paper
  • First Online:
Critical Systems: Formal Methods and Automated Verification (AVoCS 2016, FMICS 2016)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9933))

Abstract

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    CENELEC EN 50126, 50128, 50129, 50159 is a series of documents regarding the safety of railway control and protection systems.

References

  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 2012

    Google Scholar 

  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)

    Article  Google Scholar 

  3. Biba, K.: Integrity Considerations for Secure Computer Systems. MITRE Co, Bedford (1977)

    Google Scholar 

  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. 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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  7. Chandra, T.D., Toueg, S.: Unreliable failure detectors for reliable distributed systems. J. ACM 43(2), 225–267 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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. 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)

    Chapter  Google Scholar 

  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 2016

    Google Scholar 

  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. 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. 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. Haxthausen, A., Peleska, J.: Formal development and verification of a distributed railway control system. IEEE Trans. Software Eng. 26(8), 687–701 (2000)

    Article  Google Scholar 

  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)

    Chapter  Google Scholar 

  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. Lamport, L., Shostak, R., Pease, M.: The Byzantine general problem. ACM Trans. Program. Lang. Syst. 4(3), 382–401 (1982)

    Article  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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. 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. Michaut, P.: Method for managing the circulation of vehicles on a railway network and related system. US patent 8820685 B2 (2014)

    Google Scholar 

  24. Ohmstede, H.: Method for reducing data in railway operation. US patent 7578485 (2009)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Article  Google Scholar 

  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)

    Chapter  Google Scholar 

  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. UIC: Virtually coupled trains. http://www.railway-energy.org/static/Virtually_coupled_trains_86.php

  30. Weiser, M.: Program slicing. IEEE Trans. Software Eng. 10(4), 352–357 (1984)

    Article  MATH  Google Scholar 

  31. Whitwam, F., Kanner, A.: Control of automatic guided vehicles without wayside interlocking. US patent 20120323411 A1 (2012)

    Google Scholar 

  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. Zimmermann, A., Hommel, G.: Towards modeling and evaluation of ETCS real-time communication and operation. J. Syst. Softw. 77(1), 47–54 (2005)

    Article  Google Scholar 

Download references

Acknowledgements

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.

Author information

Authors and Affiliations

  1. DTU Compute, Lyngby, Denmark

    Alessandro Fantechi

  2. University of Florence - DINFO, Florence, Italy

    Alessandro Fantechi

Authors
  1. Alessandro Fantechi
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Alessandro Fantechi .

Editor information

Editors and Affiliations

  1. ISTI-CNR , Pisa, Italy

    Maurice H. ter Beek

  2. ISTI-CNR , Pisa, Italy

    Stefania Gnesi

  3. Universität Augsburg, Augsburg, Germany

    Alexander Knapp

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this paper

Cite this paper

Fantechi, A. (2016). Formal Techniques for a Data-Driven Certification of Advanced Railway Signalling Systems. In: ter Beek, M., Gnesi, S., Knapp, A. (eds) Critical Systems: Formal Methods and Automated Verification. AVoCS FMICS 2016 2016. Lecture Notes in Computer Science(), vol 9933. Springer, Cham. https://doi.org/10.1007/978-3-319-45943-1_16

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-45943-1_16

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-45942-4

  • Online ISBN: 978-3-319-45943-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation