Abstract
We report on the inclusion of a formal method into an industrial design process. Concretely, we suggest carrying out a verification step in railway interlocking design between programming the interlocking and testing this program. Safety still relies on testing, but the burden of guaranteeing completeness and correctness of the validation is in this way greatly reduced. We present a complete methodology for carrying out this verification step in the case of ladder logic programs and give results for real world railway interlockings. As this verification step reduces costs for testing, Invensys Rail is working to include such a verification step into their design process of solid state interlockings.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Abdulla, P.A., Deneux, J., Stålmarck, G., Ågren, H., Åkerlund, O.: Designing safe, reliable systems using scade. In: Margaria, T., Steffen, B. (eds.) ISoLA 2004. LNCS, vol. 4313, pp. 115–129. Springer, Heidelberg (2006)
Caspi, P., Pilaud, D., Halbwachs, N., Plaice, J.A.: LUSTRE: a declarative language for real-time programming. In: Proceedings of POPL’87, pp. 178–188 (1987)
Cimatti, A., Giunchiglia, F., Mongardi, G., Romano, D.: Formal verification of a railway interlocking system using model checking. FACS 10(4), 361–380 (1998). Springer
Claessen, K., Sorensson, N.: New techniques that improve mace-style finite model finding. In: Proceedings of CADE’03 Workshop: Model Computation (2003)
Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Meth. Syst. Des. 19(1), 7–34 (2001). Kluwer
Een, N., Sörensson, N.: Temporal induction by incremental SAT solving. ENTCS 89(4), 543–560 (2003)
Fokkink, W., Hollingshead, P.: Verification of interlockings: from control tables to ladder logic diagrams. In: Proceedings of FMICS’98, pp. 171–185 (1998)
Groote, J., Koorn, J., Van Vlijmen, S.: The safety guaranteeing system at station Hoorn-Kersenboogerd. In: Proceedings of Compass’95, pp. 57–68 (1995)
Han, K., Park, J.: Object-oriented ladder logic development framework based on the unified modeling language. In: Lee, R., Hu, G., Miao, H. (eds.) Computer and Information Science 2009. SCI, vol. 208, pp. 33–45. Springer, Heidelberg (2009)
Haxthausen, A.: Automated generation of formal safety conditions from railway interlocking tables. STTT. Springer (to appear)
IEC 61131–3 edition 2.0 2003–01. International standard. Programmable controllers. Part 3: Programming languages (January 2003)
James, P.: SAT-based model checking and its applications to train control software. MRes Thesis, Swansea University (2010)
James, P., Roggenbach, M.: Automatically verifying railway interlockings using SAT-based model checking. In: Proceedings of AVoCS’10. Electronic Communications of EASST 35 (2010)
Kanso, K.: Formal verification of ladder logic. MRes Thesis, Swansea University (2009)
Kanso, K.: Agda as a platform for the development of verified railway interlocking systems. Ph.D Thesis, Swansea University (2012)
Kanso, K., Moller, F., Setzer, A.: Automated verification of signalling principles in railway interlocking systems. ENTCS 250, 19–31 (2009)
Kanso, K., Setzer, A.: Specifying railway interlocking systems. In: Proceedings of AVoCS’09, pp. 233–236 (2009)
Kanso, K., Setzer, A.: Integrating automated and interactive theorem proving in type theory. In: Proceedings of AVoCS’10 (2010)
Lawrence, A.: Verification of railway interlockings in SCADE. MRes Thesis, Swansea University (2011)
Lawrence, A., Seisenberger, M.: Verification of railway interlockings in SCADE. In: Proceedings of AVoCS’10 (2010)
Leach, M. (ed.): Railway Control Systems: A Sequel to Railway Signalling. A & C Black, London (1991)
Minisat. http://minisat.se
Rausch, M., Krogh, B.: Formal verification of PLC programs. In: Proceedings of the American Control Conference. IEEE (1998)
Stålmarck, G.: System for determining propositional logic theorems by applying values and rules to triplets that are generated from boolean formula. US patent: 5,276,897 (1994)
The TPTP problem library for automated theorem proving. http://www.cs.miami.edu/tptp/
Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Ina Structures in Constructive Mathematics and Mathematical Logic, Steklov Mathematical Institute (1968)
Vincenti, W.G.: What Engineers Know and How They Know It. The Johns Hopkins University Press, Baltimore (1990)
Zoubek, B., Roussel, J.-M., Kwiatkowska, M.: Towards automatic verification of ladder logic programs. In: Proceedings of CESA’03. Springer (2003)
Acknowledgments
Our thanks go to Ulrich Berger for advice on the semantics of ladder logic formulae.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
James, P. et al. (2014). Verification of Solid State Interlocking Programs. In: Counsell, S., Núñez, M. (eds) Software Engineering and Formal Methods. SEFM 2013. Lecture Notes in Computer Science(), vol 8368. Springer, Cham. https://doi.org/10.1007/978-3-319-05032-4_19
Download citation
DOI: https://doi.org/10.1007/978-3-319-05032-4_19
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-05031-7
Online ISBN: 978-3-319-05032-4
eBook Packages: Computer ScienceComputer Science (R0)