Skip to main content
SpringerLink
Log in

Stepwise development and model checking of a distributed interlocking system using RAISE

  • Original Article
  • Published:
Formal Aspects of Computing

Abstract

This paper considers the challenge of designing and verifying control protocols for geographically distributed railway interlocking systems. It describes how this challenge can be tackled by stepwise development and model checking of state transition system models in a new extension of the RAISE Specification Language.

Railway interlocking systems are reconfigurable systems which can be configured by supplying data describing the network to be controlled and other details. Therefore, such systems are natural candidates for being modelled by generic state transition systems, which abstract away from the concrete configuration at the time of modelling, and can later be instantiated with concrete data.

For a real-world case study, a generic state transition system is developed in steps, starting with an abstract model of the essential system behaviour and incrementally adding details and restrictions. The stepwise development method allows different variants of the control protocol to be explored. The generic models are instantiated with concrete configuration data, after which desired properties, in particular safety properties, of the system models are verified using model checking.

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

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Abrial, J.-R.: On B and Event-B: principles, success and challenges. In: Butler, M., Raschke, A., Hoang, T.S., Reichl, K. (eds.) Abstract State Machines, Alloy, B, TLA, VDM, and Z, pp. 31–35. Springer, Cham (2018)

    Chapter  Google Scholar 

  2. Basile, D., ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F., Piattino, A., Trentini, D., Ferrari, A.: On the industrial uptake of formal methods in the railway domain–a survey with stakeholders. In: Furia, C.A., Winter, K. (eds.) Integrated formal methods. Lecture notes in computer science, vol. 11023, pp. 20–29. Cham, Springer (2018)

    Chapter  Google Scholar 

  3. Basile D, ter Beek MH, Ferrari A, Legay A (2019) Modelling and analysing ERTMS L3 moving block railway signalling with Simulink and Uppaal SMC. In: Larsen KG, Willemse T (eds) Formal methods for industrial critical systems, volume 11687 of Lecture notes in computer science, pp 1–21. Springer, Cham

  4. Butler, M.: Decomposition structures for Event-B. In: Leuschel, M., Wehrheim, H. (eds.) Integrated formal methods. Lecture notes in computer science, vol. 5423, pp. 20–38. Berlin, Springer (2009)

    Chapter  Google Scholar 

  5. Comptier M, Deharbe D, Perez JM, Mussat L, Pierre T, Sabatier D (2017) Safety analysis of a CBTC system: a rigorous approach with Event-B. In: Fantechi A, Lecomte T, Romanovsky A (eds) Reliability, safety, and security of railway systems. Modelling, analysis, verification, and certification, volume 10598 of Lecture notes in computer science, pp 148–159. Springer, Cham

  6. Comptier M, Leuschel M, Mejia LF, Perez JM, Mutz M (2019) Property-based modelling and validation of a CBTC zone controller in Event-B. In: Collart-Dutilleul S, Lecomte T, Romanovsky A (eds) Reliability, safety, and security of railway systems. modelling, analysis, verification, and certification, volume 11495 of Lecture notes in computer science, pp 202–212. Springer, Cham

  7. CENELEC European Committee for Electrotechnical Standardization (2011) EN 50128:2011—railway applications—communications, signalling and processing systems—software for railway control and protection systems

  8. Fantechi A (2012) Distributing the challenge of model checking interlocking control tables. In: Margaria T, Steffen B (eds) Leveraging applications of formal methods, verification and validation. Applications and case studies, volume 7610 of Lecture notes in computer science, pp 276–289. Springer, Cham

  9. Fantechi, A.: Twenty-five years of formal methods and railways: what next? In: Counsell, S., Núñez, M. (eds.) Software engineering and formal methods. Lecture notes in computer science, vol. 8368, pp. 167–183. Cham, Springer (2014)

    Chapter  Google Scholar 

  10. Fantechi A, Gnesi S, Haxthausen A, van de Pol J, Roveri M, Treharne H (2016) SaRDIn—a safe reconfigurable distributed interlocking. In: Proceedings of the 11th world congress on railway research (WCRR 2016). Milano, Ferrovie dello Stato Italiane

  11. Fantechi, A., Haxthausen, A.E.: Safety interlocking as a distributed mutual exclusion problem. In: Howar, F., Barnat, J. (eds.) Formal methods for industrial critical systems. Lecture notes in computer science, vol. 11119, pp. 52–66. Cham, Springer (2018)

    Chapter  Google Scholar 

  12. Fantechi, A., Haxthausen, A.E., Macedo, H.D.: Compositional verification of interlocking systems for large stations. In: Cimatti, A., Sirjani, M. (eds.) International conference on software engineering and formal methods. 10469 of Lecture notes in computer science, vol. of, pp. 236–252. Cham, Springer (2017)

    Chapter  Google Scholar 

  13. Fantechi A, Haxthausen AE, Nielsen MBR (2017) Model checking geographically distributed interlocking systems using UMC. In: 2017 25th Euromicro international conference on parallel, distributed and network-based processing (PDP), pp 278–286

  14. Ferrari, A., Magnani, G., Grasso, D., Fantechi, A.: Model checking interlocking control tables. In: Schnieder, E., Tarnai, G. (eds.) FORMS/FORMAT 2010–formal methods for automation and safety in railway and automotive systems, pp. 107–115. Springer, Cham (2010)

    Google Scholar 

  15. George C (2003) The development of the RAISE tools. In: Aichernig BK, Maibaum T (eds) Formal methods at the crossroads. From Panacea to foundational support: 10th anniversary colloquium of UNU/IIST, the International Institute for Software Technology of The United Nations University, Lisbon, Portugal, March 18–20: Revised papers, pp. 49–64. Springer, Berlin (2002)

    Google Scholar 

  16. Geisler, S., Haxthausen, A.E.: Stepwise development and model checking of a distributed interlocking system–using RAISE. In: Havelund, K., Peleska, J., Roscoe, B., de Vink, E. (eds.) Formal methods. Lecture notes in computer science, vol. 10951, pp. 277–293. Cham, Springer (2018)

    Chapter  Google Scholar 

  17. Haxthausen AE (2014) Automated generation of formal safety conditions from railway interlocking tables. Int J Softw Tools Technol Transf (STTT), Spec Issue Form Methods Railw Control Syst 16(6):713–726

  18. Anne E. Haxthausen, Marie Le Bliguet, and Andreas A. Kjær. Modelling and Verification of Relay Interlocking Systems. In Christine Choppy and Oleg Sokolsky, editors, 15th Monterey Workshop: Foundations of Computer Software, Future Trends and Techniques for Development, volume 6028 of Lecture Notes in Computer Science, pages 141–153. Springer, 2010.

  19. Thai Son Hoang, Michael Butler, and Klaus Reichl. The hybrid ERTMS/ETCS level 3 case study. In Michael Butler, Alexander Raschke, Thai Son Hoang, and Klaus Reichl, editors, Abstract State Machines, Alloy, B, TLA, VDM, and Z, volume 10817 of Lecture Notes in Computer Science, pages 251–261. Springer Verlag, 2018.

  20. Haxthausen, A.E., Hede, K.: Formal verification of railway timetables–using the UPPAAL model checker. In: ter Beek, M.H., Fantechi, A., Semini, L. (eds.) From software engineering to formal methods and tools, and back: essays dedicated to Stefania Gnesi on the occasion of Her 65th Birthday. Lecture notes in computer science, vol. 11865, pp. 433–448. Cham, Springer International Publishing (2019)

    Chapter  Google Scholar 

  21. Anne E. Haxthausen and Peter H. Østergaard. On the use of static checking in the verification of interlocking systems. In Tiziana Margaria and Bernhard Steffen, editors, Leveraging Applications of Formal Methods, Verification and Validation, volume 9953 of Lecture Notes in Computer Science. Springer, 2016.

  22. Haxthausen, A.E., Peleska, J.: Formal development and verification of a distributed railway control systems. IEEE Trans Softw Eng 26(8), 687–701 (2000)

    Article  Google Scholar 

  23. James P, Möller F, Nguyen HN, Roggenbach M, Schneider S, Treharne H, Trumble M, Williams D (2014) Verification of scheme plans using CSP\(||\)B. In: Counsell S, Núñez M (eds) Software engineering and formal methods, volume 8368 of Lecture notes in computer science, pp 189–204. Springer

  24. James P, Möller F, Nguyen HN, Roggenbach M (2014) Steve Schneider, and Helen Treharne. Techniques for modelling and verifying railway interlockings. Int J Softw Tools Technol Transf 16(6):685–711

  25. Limbrée C, Cappart Q, Pecheur C, Tonetta S (2016) Verification of Railway Interlocking - Compositional Approach with OCRA. In: Lecomte T, Pinger R, Romanovsky A (eds) Reliability, safety, and security of railway Systems. Modelling, analysis, verification, and certification. RSSRail 2016. Lecture Notes in Computer Science, vol 9707, pp 134–149. Springer, Cham

  26. Luteberget, B., Johansen, C.: Efficient verification of railway infrastructure designs against standard regulations. Form Methods Syst Des 52(1), 1–32 (2018)

    Article  Google Scholar 

  27. Merz, S.: The specification language TLA+, pp. 401–451. Springer, Berlin (2008)

    Google Scholar 

  28. Mammar, A., Frappier, M., Tueno Fotso, S.J., Laleau, R.: An Event-B model of the hybrid ERTMS/ETCS level 3 standard. In: Butler, M., Raschke, A., Hoang, T.S., Reichl, K. (eds.) Abstract State Machines, Alloy, B, TLA, VDM, and Z, pp. 353–366. Springer, Cham (2018)

    Chapter  Google Scholar 

  29. Perna JI, George C (2007) Model checking RAISE applicative specifications. In: Proceedings of the fifth IEEE international conference on software engineering and formal methods, 2007, pp 257–268. IEEE Computer Society Press

  30. Peleska J, Krafczyk N, Haxthausen AE, Pinger R (2019) Efficient data validation for geographical interlocking systems. In: Reliability, safety, and security of railway systems. Modelling, analysis, verification, and certification, pp 142–158

  31. The RAISE Language Group, George C, Haff P, Havelund K, Haxthausen AE, Milne R, Bendix Nielsen C, Prehn S, Wagner KR: The RAISE Specification Language. The BCS Practitioners Series, Prentice Hall Int (1992)

    Google Scholar 

  32. Klaus Reichl, Tomas Fischer, and Peter Tummeltshammer. Using formal methods for verification and validation in railway. In Bernhard K. Aichernig and Carlo A. Furia, editors, Tests and Proofs, volume 9762 of Lecture Notes in Computer Science, pages 3–13. Springer Verlag, 2016.

  33. Sabatier D (2016) Using formal proof and B method at system level for industrial projects. In: Lecomte T, Pinger R, Romanovsky A (eds) Reliability, safety, and security of railway systems. Modelling, analysis, verification, and certification, volume 9707 of Lecture notes in computer science, pp 20–31. Springer Verlag

  34. Symbolic Analysis Laboratory, SAL, Home page (2001). http://sal.csl.sri.com. Accessed 6 Feb 2020

  35. ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: A state/event-based model-checking approach for the analysis of abstract system properties. Sci Comput Program 76(2), 119–135 (2011)

    Article  Google Scholar 

  36. UMC homepage. http://fmt.isti.cnr.it/umc/V4.2/umc.html. Accessed 6 Feb 2020

  37. Verified Systems International GmbH (2013) RT-tester model-based test case and test data generator—RTT-MBT—user manual. Available on request from http://www.verified.de. Accessed 6 Feb 2020

  38. Vu LH, Haxthausen AE, Peleska J (2017) Formal modelling and verification of interlocking systems featuring sequential release. Sci Comput Program 133(Part 2):91–115. https://doi.org/10.1016/j.scico.2016.05.010

  39. Winter K (2002) Model checking railway interlocking systems. In: Proceedings of the twenty-fifth australasian computer science conference (ACSC2002), pp 303–310

Download references

Acknowledgements

The authors would like to express their gratitude to Jan Peleska fromwhomthe case study originates and together with whom the second author had the great pleasure to verify the same case study by theorem proving [HP00]. We would also like to thank him and the reviewers for very useful comments to a draft of this paper.

Author information

Authors and Affiliations

  1. DTU Compute, Technical University of Denmark, Kongens Lyngby, Denmark

    S. Geisler & A. E. Haxthausen

Authors
  1. S. Geisler
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. A. E. Haxthausen
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to S. Geisler.

Additional information

Erik de Vink, Ana Cavalcanti, Jan Peleska, Bill Roscoe, and Cliff Jones

Publisher’s Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Geisler, S., Haxthausen, A.E. Stepwise development and model checking of a distributed interlocking system using RAISE. Form Asp Comp 33, 87–125 (2021). https://doi.org/10.1007/s00165-020-00507-2

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s00165-020-00507-2

Keywords

Search

Navigation