Skip to main content
SpringerLink
Log in

Stepwise Development and Model Checking of a Distributed Interlocking System - Using RAISE

  • Conference paper
  • First Online:
Formal Methods (FM 2018)

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

Included in the following conference series:

Abstract

This paper considers the challenge of designing and verifying control protocols for geographically distributed railway interlocking systems. It describes for a real-world case study how this can be tackled by stepwise development and model checking of state transition models in an extension of the RAISE Specification Language (RSL). This method also allows different variants of the control protocols to be explored.

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 79.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 99.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.

    As the model is generic, the number of components is not yet known, so we can’t specify a variable for each component holding its local state. Instead we use maps as shown above.

  2. 2.

    Since only one event should be allowed at the same time in this model, it is sufficient to store a segment rather than a map from trains to segments, where for each train t, tmpSeg(t) could hold data sent by t.

  3. 3.

    For this variable there is a similar comment as for tmpSeg.

  4. 4.

    It is this condition which enforces the atomic event refinement.

References

  1. Symbolic Analysis Laboratory, SAL (2001). http://sal.csl.sri.com

  2. CENELEC European Committee for Electrotechnical Standardization. EN 50128:2011 - Railway applications - Communications, signalling and processing systems - Software for railway control and protection systems (2011)

    Google Scholar 

  3. Fantechi, A., Gnesi, S., Haxthausen, A., van de Pol, J., Roveri, M., Treharne, H.: SaRDIn - a safe reconfigurable distributed interlocking. In: Proceedings 11th World Congress on Railway Research (WCRR 2016). Ferrovie dello Stato Italiane, Milano (2016)

    Google Scholar 

  4. Fantechi, A., Haxthausen, A.E., Nielsen, M.B.R.: 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 (2017)

    Google Scholar 

  5. 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). https://doi.org/10.1007/978-3-642-14261-1_11

    Chapter  Google Scholar 

  6. Haxthausen, A.E., Automated generation of formal safety conditions from railway interlocking tables. Int. J. Softw. Tools Technol. Transf. (STTT) 16(6), 713–726 (2014). Special Issue on Formal Methods for Railway Control Systems

    Article  Google Scholar 

  7. Haxthausen, A.E., Le Bliguet, M., Kjær, A.A.: Modelling and verification of relay interlocking systems. In: Choppy, C., Sokolsky, O. (eds.) Monterey Workshop 2008. LNCS, vol. 6028, pp. 141–153. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-12566-9_8

    Chapter  Google Scholar 

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

    Article  Google Scholar 

  9. James, P., et al.: Verification of scheme plans using CSP\(||\)B. In: Counsell, Steve, Núñez, Manuel (eds.) SEFM 2013. LNCS, vol. 8368, pp. 189–204. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-05032-4_15

    Chapter  Google Scholar 

  10. Perna, J.I., George, C.: Model checking RAISE applicative specifications. In: Proceedings of the Fifth IEEE International Conference on Software Engineering and Formal Methods, pp. 257–268. IEEE Computer Society Press (2007)

    Google Scholar 

  11. The RAISE Language Group: George, C., Haff, P., Havelund, K., Haxthausen, A.E., Milne, R., Nielsen, C.B., Prehn, S., Wagner, K.R.: The RAISE Specification Language. The BCS Practitioners Series. Prentice Hall Int., Englewood Cliffs (1992)

    Google Scholar 

  12. Verified Systems International GmbH. RT-Tester Model-Based Test Case and Test Data Generator - RTT-MBT - User Manual (2013). http://www.verified.de

  13. Vu, L.H., Haxthausen, A.E., Peleska, J.: Formal modelling and verification of interlocking systems featuring sequential release. Sci. Comput. Programm. 133(2), 91–115 (2017). https://doi.org/10.1016/j.scico.2016.05.010

    Article  Google Scholar 

  14. Winter, K.: Model checking railway interlocking systems. In: Proceedings of Twenty-Fifth Australasian Computer Science Conference (ACSC 2002), pp. 303–310 (2002)

    Google Scholar 

Download references

Acknowledgements

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

Author information

Authors and Affiliations

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

    Signe Geisler & Anne E. Haxthausen

Authors
  1. Signe Geisler
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Anne E. Haxthausen
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Signe Geisler .

Editor information

Editors and Affiliations

  1. NASA Jet Propulsion Laboratory, Pasadena, California, USA

    Klaus Havelund

  2. University of Bremen, Bremen, Germany

    Jan Peleska

  3. University of Oxford, Oxford, United Kingdom

    Bill Roscoe

  4. Eindhoven University of Technology, Eindhoven, The Netherlands

    Erik de Vink

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Geisler, S., Haxthausen, A.E. (2018). 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. FM 2018. Lecture Notes in Computer Science(), vol 10951. Springer, Cham. https://doi.org/10.1007/978-3-319-95582-7_16

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-95582-7_16

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-95581-0

  • Online ISBN: 978-3-319-95582-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation