Skip to main content
SpringerLink
Log in

Optimising Ordering Strategies for Symbolic Model Checking of Railway Interlockings

  • Conference paper
Book cover 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

Interlockings implement Railway Signalling Principles which ensure the safe movements of trains along a track system. They are safety critical systems which require a thorough analysis. We are aiming at supporting the safety analysis by automated tools, namely model checkers.

Model checking provides a full state space exploration and is thus intrinsically limited in the problem’s state space. Current research focuses on extending these limits and pushing the boundaries. In our work we investigate possible optimisations for symbolic model checking. Symbolic model checkers exploit a compact representation of the model using Binary Decision Diagram. These structures provide a canonical representation which allows for reductions. The compactness of this data structure and possible reductions are dependent on two orderings: the ordering of variables and the ordering in which sub-structures are manipulated. This paper reports on findings of how a near to optimal ordering can be generated for the domain of interlocking verification.

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. Robinson, N., Barney, D., Kearney, P., Nikandros, G., Tombs, D.: Automatic generation and verification of design specification. In: Proc. of Int. Symp. of the International Council on Systems Engineering, INCOSE 2001 (2001)

    Google Scholar 

  2. Gnesi, S., Lenzini, G., Latella, D., Abbaneo, C., Amendola, A., Marmo, P.: An automatic SPIN validation of a safety critical railway control system. In: Procs. of IEEE Conference on Dependable Systems and Networks, pp. 119–124. IEEE Computer Society (2000)

    Google Scholar 

  3. Bernardeschi, C., Fantechi, A., Gnesi, S., Mongardi, G.: Proving Safety Properties for Embedded Control Systems. In: Hlawiczka, A., Simoncini, L., Silva, J.G.S. (eds.) EDCC 1996. LNCS, vol. 1150, pp. 321–332. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  4. Cleaveland, R., Luettgen, G., Natarajan, V.: Modeling and Verifying Distributed Systems Using Priorities: A case Study. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 287–297. Springer, Heidelberg (1996)

    Google Scholar 

  5. Groote, J., Koorn, J., van Vlijmen, S.: The safety guaranteeing system at station Hoorn-Kersenboogerd. In: Proceedings 10th IEEE Conference on Computer Assurance (COMPASS 1995), pp. 131–150. IEEE Computer Society Press (1995)

    Google Scholar 

  6. Eisner, C.: Using Symbolic Model Checking to Verify the Railway Stations of Hoorn-Kersenboogerd and Heerhugowaard. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 97–109. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  7. Eisner, C.: Using symbolic CTL model checking to verify the railway stations of Hoorn-Kersenboogerd and Heerhugowaard. Software Tools for Technology Transfer 4(1), 107–124 (2002)

    Article  Google Scholar 

  8. Simpson, A., Woodcock, J., Davies, J.: The mechanical verification of solid state interlocking geographic data. In: Groves, L., Reeves, S. (eds.) Proc. of Formal Methods Pacific (FMP 1997). Discrete Mathematics and Theoretical Computer Science Series, pp. 223–243. Springer (1997)

    Google Scholar 

  9. Huber, M., King, S.: Towards an Integrated Model Checker for Railway Signalling Data. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 204–223. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  10. Ferrari, A., Magnani, G., Grasso, D., Fantechi, A.: Model checking interlocking control tables. In: Schnieder, E., Tarnai, G. (eds.) Proceedings of Conference on Formal Methods for Automation and Safety in Railway and Automotive Systems (FORMS/FORMAT 2010), vol. 2, pp. 107–115. Springer (2011)

    Google Scholar 

  11. Winter, K., Robinson, N.J.: Modelling large railway interlockings and model checking small ones. In: Oudshoorn, M. (ed.) Proc. of Australasian Computer Science Conference, ACSC 2003 (2003)

    Google Scholar 

  12. Winter, K., Johnston, W., Robinson, P., Strooper, P., van den Berg, L.: Tool support for checking railway interlocking designs. In: Cant, T. (ed.) Proc. of the 10th Australian Workshop on Safety Related Programmable Systems (SCS 2005), vol. 55, pp. 101–107. Australian Computer Society, Inc. (2005)

    Google Scholar 

  13. Johnston, W., Winter, K., van den Berg, L., Strooper, P., Robinson, P.: Model-Based Variable and Transition Orderings for Efficient Symbolic Model Checking. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 524–540. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

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

    Google Scholar 

  15. Robinson, N.: Operation concept document. SigTools-004, version 1.9 (May 2002)

    Google Scholar 

  16. Robinson, N.: Design specification – Track Layout Editor. SigTools-032, version 1.1 (April 2004)

    Google Scholar 

  17. McComb, T., Robinson, N.J.: Assuring graphical computer aided design tools. Technical Report TR02-18, Software Verification Research Centre, University of Queensland (2001)

    Google Scholar 

  18. Tombs, D., Robinson, N.J., Nikandros, G.: Signalling control table generation and verification. In: Proc. of Conf. on Railway Engineering (CORE 2002). Railway Technical Society of Australasia (2002)

    Google Scholar 

  19. Johnston, W.: Design specification – Control Table Editor. SigTools-044, version 0.1 (January 2003)

    Google Scholar 

  20. van den Berg, L., Strooper, P., Johnston, W.: An automated approach for the interpretation of counter-examples. In: Bloem, R., Roveri, M., Somenzi, F. (eds.) Proceedings of 1st Workshop on Verification and Debugging, pp. 6–25 (2006)

    Google Scholar 

  21. Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An OpenSource Tool for Symbolic Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  22. Egon Börger, R.S.: Abstract State Machines: A Method for High-Level System Design and Analysis. Springer (2003)

    Google Scholar 

  23. Cavda, R., Cimatti, A., Jochim, C.A., Keighren, G., Olivetti, E., Pistore, M., Roveri, M., Tchaltsev, A.: NuSMV 2.5 User Manual (2010), http://nusmv.irst.itc.it

  24. Winter, K.: Model checking control tables: the ASM-NuSMV approach. SigTools.039, version 0.1 (October 2002)

    Google Scholar 

  25. Johnston, W.: Design specification - Verification Manager and NuSMV Driver. SigTools-051, version 0.4 (April 2004)

    Google Scholar 

  26. Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  27. Schneider, S.: An operational semantics for timed CSP. Information and Computation 116(2), 193–213 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  28. van den Berg, L., Strooper, P., Winter, K.: Introducing Time in an Industrial Application of Model-Checking. In: Leue, S., Merino, P. (eds.) FMICS 2007. LNCS, vol. 4916, pp. 56–67. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  29. Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers C-35(8) (August 1986)

    Google Scholar 

  30. Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press (2000)

    Google Scholar 

  31. Lewis, G., Comella-Dorda, S., Gluch, D., Hudak, J., Weinstock, C.: Model-based verification: Analysis guidelines. Technical Report CMU/SEI-2001-TN-028, Carnegie Mellon Software Engineering Institute (2001)

    Google Scholar 

  32. Burch, J., Clarke, E., Long, D.: Symbolic model checking with partitioned transition relations. In: Int. Conf. on Very Large Scale Integration (1991)

    Google Scholar 

  33. Geist, D., Beer, I.: Efficient Model Checking by Automated Ordering of Transition Relation. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 299–310. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  34. McMillan, K.: Symbolic Model Checking. Kluwer Academic Publishers (1993)

    Google Scholar 

  35. Moon, I.-H., Hachtel, G.D., Somenzi, F.: Border-Block Triangular Form and Conjunction Schedule in Image Computation. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 73–90. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Information Technology and Electrical Engineering, The University of Queensland, St.Lucia, QLD, 4072, Australia

    Kirsten Winter

Authors
  1. Kirsten Winter
    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

Winter, K. (2012). Optimising Ordering Strategies for Symbolic Model Checking of Railway Interlockings. 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_24

Download citation

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

  • 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