Skip to main content
SpringerLink
Log in

Automated Generation of Safety Requirements from Railway Interlocking Tables

  • Conference paper
Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies (ISoLA 2012)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 7610))

Abstract

This paper describes a tool for extracting formal safety conditions from interlocking tables for railway interlocking systems. The tool has been applied to generate safety conditions for the interlocking system at Stenstrup station in Denmark, and the generated conditions were then checked to hold by the SAL model checker tool.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

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

  2. Aanæs, M., Thai, H.P.: Modelling and Verification of Relay Interlocking Systems. Technical Report IMM-MSC-2012-14, DTU Informatics, Technical University of Denmark, Master thesis supervised by Anne Haxthausen, ah@imm.dtu.dk (2012)

    Google Scholar 

  3. Bjørner, D.: New Results and Current Trends in Formal Techniques for the Development of Software for Transportation Systems. In: Proceedings of the Symposium on Formal Methods for Railway Operation and Control Systems (FORMS 2003), Budapest, Hungary, May 15-16, L’Harmattan Hongrie (2003)

    Google Scholar 

  4. Bliguet, M.L., Kjær, A.A.: Modelling Interlocking Systems for Railway Stations. Technical Report IMM-M.Sc.-2008-68, DTU Informatics, Technical University of Denmark, Master thesis supervised by Anne Haxthausen, ah@imm.dtu.dk (2008)

    Google Scholar 

  5. Cao, Y., Xu, T., Tang, T., Wang, H., Zhao, L.: Automatic Generation and Verification of Interlocking Tables Based on Domain Specific Language for Computer Based Interlocking Systems (DSL-CBI). In: Proceedings of the IEEE International Conference on Computer Science and Automation Engineering (CSAE 2011), pp. 511–515. IEEE (2011)

    Google Scholar 

  6. Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press (1999)

    Google Scholar 

  7. Eriksson, L.-H.: Using Formal Methods in a Retrospective Safety Case. In: Heisel, M., Liggesmeyer, P., Wittmann, S. (eds.) SAFECOMP 2004. LNCS, vol. 3219, pp. 31–44. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  8. Fantechi, A.: The Role of Formal Methods in Software Development for Railway Applications. In: Railway Safety, Reliability and Security: Technologies and System Engineering, pp. 282–297. IGI Global (2012)

    Google Scholar 

  9. Ferrari, A., Magnani, G., Grasso, D., Fantechi, A.: Model Checking Interlocking Control Tables. In: Schnieder, E., Tarnai, G. (eds.) Proceedings of Formal Methods for Automation and Safety in Railway and Automotive Systems (FORMS/FORMAT 2010)), Braunschweig, Germany. Springer (2011)

    Google Scholar 

  10. Haxthausen, A.E.: Towards a Framework for Modelling and Verification of Relay Interlocking Systems. In: Calinescu, R., Jackson, E. (eds.) Monterey Workshop 2010. LNCS, vol. 6662, pp. 176–192. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  11. Haxthausen, A.E., Kjær, A.A., Le Bliguet, M.: Formal Development of a Tool for Automated Modelling and Verification of Relay Interlocking Systems. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 118–132. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  12. Haxthausen, A.E., Peleska, J., Kinder, S.: A Formal Approach for the Construction and Verification of Railway Control Systems. Formal Aspects of Computing 23(2), 191–219 (2011), The article is also available electronically on SpringerLink, http://www.springerlink.com/openurl.asp?genre=article&id=doi:10.1007/s00165-009-0143-6

  13. Mirabadi, A., Yazdi, M.B.: Automatic Generation and Verification of Railway Interlocking Control Tables using FSM and NuSMV. Transportation Problems, 103–110 (2009)

    Google Scholar 

  14. Schnieder, E., Tarnai, G. (eds.): Proceedings of Formal Methods for Automation and Safety in Railway and Automotive Systems (FORMS/FORMAT 2010), Braunschweig, Germany. Springer (2011)

    Google Scholar 

  15. The RAISE Language Group. The RAISE Specification Language. The BCS Practitioners Series. Prentice Hall Int. (1992)

    Google Scholar 

  16. The RAISE Method Group. The RAISE Development Method. The BCS Practitioners Series. Prentice Hall Int. (1995)

    Google Scholar 

  17. Winter, K.: Symbolic Model Checking for Interlocking Systems. In: Railway Safety, Reliability and Security: Technologies and System Engineering, pp. 298–315. IGI Global (2012)

    Google Scholar 

  18. Winter, K., Johnston, W., Robinson, P., Strooper, P., van den Berg, L.: Tool Support for Checking Railway Interlocking Designs. In: Proceedings of the 10th Australian Workshop on Safety Critical Systems and Software, SCS 2005, Darlinghurst, Australia, Australia, vol. 55, pp. 101–107. Australian Computer Society, Inc. (2006)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. DTU Informatics, Technical University of Denmark, DK-2800, Lyngby, Denmark

    Anne E. Haxthausen

Authors
  1. Anne E. Haxthausen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institut für Informatik, Universität Potsdam, August-Bebel-Straße 89, 14482, Potsdam, Germany

    Tiziana Margaria

  2. Fakultät für Informatik, Technische Universität Dortmund, Otto-Hahn-Straße 14, 44227, Dortmund, Germany

    Bernhard Steffen

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Haxthausen, A.E. (2012). Automated Generation of Safety Requirements from Railway Interlocking Tables. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies. ISoLA 2012. Lecture Notes in Computer Science, vol 7610. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-34032-1_25

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-34032-1_25

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-34031-4

  • Online ISBN: 978-3-642-34032-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation