Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Leveraging Applications of Formal Methods

ISoLA 2016: Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications pp 266–278Cite as

On the Use of Static Checking in the Verification of Interlocking Systems

  • Conference paper
  • First Online:

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

Abstract

In the formal methods community, the correctness of interlocking tables is typically verified by model checking. This paper suggests to use a static checker for this purpose and it demonstrates for the RobustRailS verification tool set that the execution time and memory usage of its static checker are much less than of its model checker. Furthermore, the error messages of the static checker are much more informative than the counter examples produced by classical model checkers.

A.E. Haxthausen and P.H. Østergaard—The authors’ research has been funded by the RobustRailS project granted by Innovation Fund Denmark.

This is a preview of subscription content, 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

Learn about institutional subscriptions

Notes

  1. 1.

    Interlocking tables are also sometimes called control tables.

  2. 2.

    http://robustrails.man.dtu.dk.

  3. 3.

    These include points in the path and overlap, and points used for flank and front protection. For detail about flank and front protection, see [16].

  4. 4.

    This essentially means that they use the same track elements. For a complete definition, see [19].

  5. 5.

    It should here be noted that using this model checker in a second step for verifying the safety of the model of the instantiated interlocking system has actually turned out to be very efficient. For instance, it succeeded to verify the EDL line, where other model checkers failed within some given resources, cf. [22].

References

  1. Banci, M., Fantechi, A., Gnesi, S.: Some Experiences on Formal Specification of Railway Interlocking Systems Using Statecharts (2005)

    Google Scholar 

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

  3. C. 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 

  4. Fantechi, A.: Twenty-five years of formal methods and railways: what next? In: Counsell, S., Núñez, M. (eds.) SEFM 2013. LNCS, vol. 8368, pp. 167–183. Springer, Heidelberg (2014). doi:10.1007/978-3-319-05032-4_13

    Chapter  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 – Formal Methods for Automation and Safety in Railway and Automotive Systems, pp. 107–115. Springer, Heidelberg (2010)

    Google Scholar 

  6. Hvid Hansen, H., Ketema, J., Luttik, B., Mousavi, M.R., Pol, J., Santos, O.M.: Automated verification of executable UML models. In: Aichernig, B.K., Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol. 6957, pp. 225–250. Springer, Heidelberg (2011). doi:10.1007/978-3-642-25271-6_12

    Chapter  Google Scholar 

  7. 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). doi:10.1007/978-3-642-21292-5_10

    Chapter  Google Scholar 

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

  9. Haxthausen, A.E., 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). doi:10.1007/978-3-642-12566-9_8

    Chapter  Google Scholar 

  10. Haxthausen, A.E., Peleska, J., Kinder, S.: A formal approach for the construction and verification of railway control systems. Formal Aspects Comput. 23(2), 191–219 (2011)

    Article  MATH  Google Scholar 

  11. 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). doi:10.1007/978-3-319-05032-4_15

    Chapter  Google Scholar 

  12. Limbrée, C., Cappart, Q., Pecheur, C., Tonetta, S.: Verification of railway interlocking - compositional approach with OCRA. In: Lecomte, T., Pinger, R., Romanovsky, A. (eds.) RSSRail 2016. LNCS, vol. 9707, pp. 134–149. Springer, Heidelberg (2016). doi:10.1007/978-3-319-33951-1_10

    Chapter  Google Scholar 

  13. Mirabadi, A., Yazdi, M.B.: Automatic generation and verification of railway interlocking control tables using FSM and NuSMV. Transp. Probl. 4, 103–110 (2009)

    Google Scholar 

  14. Peleska, J.: Industrial-strength model-based testing - state of the art and current challenges. In: Petrenko, A.K., Schlingloff, H. (eds.) Proceedings 8th Workshop on Model-Based Testing. Electronic Proceedings in Theoretical Computer Science, vol. 111, pp. 3–28. Open Publishing Association, Rome (2013)

    Google Scholar 

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

    Google Scholar 

  16. Theeg, G., Vlasenko, S.V., Anders, E.: Railway Signalling & Interlocking: International Compendium. Eurailpress, Germany (2009)

    Google Scholar 

  17. Tombs, D., Robinson, N., Nikandros, G.: Signalling control table generation and verification. In: CORE 2002: Cost Efficient Railways through Engineering, p. 415. Railway Technical Society of Australasia/Rail Track Association of Australia (2002)

    Google Scholar 

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

  19. Vu, L.H.: Formal Development and Verification of Railway Control Systems - In the context of ERTMS/ETCS Level 2. Ph.D. thesis, Technical University of Denmark, DTU Compute (2015)

    Google Scholar 

  20. Vu, L.H., Haxthausen, A.E., Peleska, J.: A domain-specific language for railway interlocking systems. In: Schnieder, E., Tarnai, G. (eds.) FORMS/FORMAT 2014–10th Symposium on Formal Methods for Automation and Safety in Railway and Automotive Systems, Institute for Traffic Safety and Automation Engineerin, pp. 200–209. Technische Universität Braunschweig (2014)

    Google Scholar 

  21. Vu, L.H., Haxthausen, A.E., Peleska, J.: Formal modeling and verification of interlocking systems featuring sequential release. In: Artho, C., Ölveczky, P.C. (eds.) Formal Techniques for Safety-Critical Systems. Communications in Computer and Information Science, vol. 476, pp. 223–238. Springer, Heidelberg (2015)

    Google Scholar 

  22. Vu, L.H., Haxthausen, A.E., Peleska, J.: Formal modeling and verification of interlocking systems featuring sequential release. Sci. Comput. Program. (2016). http://dx.doi.org/10.1016/j.scico.2016.05.010

  23. 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, vol. 55, pp. 101–107. Australian Computer Society, Inc., Darlinghurst (2006)

    Google Scholar 

Download references

Acknowledgements

The authors would like to express their gratitude to (1) Jan Peleska and Linh Hong Vu for the excellent contribution to the development of the RobustRailS interlocking verification method and tool set (including the static checker discussed in this paper) and for an always very enjoyable collaboration, (2) Ross Edwin Gammon and Nikhil Mohan Pande from Banedanmark and Jan Bertelsen from Thales for helping with their expertise about Danish interlocking systems, and (3) Uwe Schulze and Florian Lapschies from the University of Bremen for their help with the implementation in the RT-Tester toolchain.

Author information

Authors and Affiliations

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

    Anne E. Haxthausen & Peter H. Østergaard

Authors
  1. Anne E. Haxthausen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Peter H. Østergaard
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Anne E. Haxthausen .

Editor information

Editors and Affiliations

  1. Lero, Limerick, Ireland

    Tiziana Margaria

  2. TU Dortmund, Dortmund, Germany

    Bernhard Steffen

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this paper

Cite this paper

Haxthausen, A.E., Østergaard, P.H. (2016). On the Use of Static Checking in the Verification of Interlocking Systems. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications. ISoLA 2016. Lecture Notes in Computer Science(), vol 9953. Springer, Cham. https://doi.org/10.1007/978-3-319-47169-3_19

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-47169-3_19

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-47168-6

  • Online ISBN: 978-3-319-47169-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation