Abstract
Geographic Data for Solid State Interlocking (SSI) systems detail site-specific behaviour of the railway interlocking. This report demonstrates how five vital safety properties of such data can be verified automatically using model checking. A prototype of a model checker for Geographic Data has been implemented by replacing the parser and compiler of NuSMV. The resulting tool, gdlSMV, directly reads Geographic Data and builds a corresponding representation on which model checking is performed using NuSMV’s symbolic model checking algorithms.
Because of the large number of elements in a typical track layout controlled by an SSI system, a number of optimisations had to be implemented in order to be able to verify the corresponding data sets.
We outline how most of the model checking can be hidden from the user, providing a simple interface that directly refers to the data being verified.
The first author joined Siemens after the work reported in this paper had been completed. Siemens did not take part in this research.
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
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Bailey, C. (ed.): European Railway Signalling. Institution of Railway Signal Engineers. A & C Black, London (1995)
Cimatti, A., Clarke, E., Giunchiglia, F. and Roveri, M.: NuSMV: a new Symbolic Model Checker. Springer: International Journal on Software Tools for Technology Transfer, Volume 2 Issue 4, pp410–425 (2000)
Cabodi, G., Camurati, P. and Quer, S.: Reachability analysis of large circuits using disjunctive partitioning and partial iterative squaring. Elsevier: Journal of Systems Architecture, Volume 47, Issue 2, pp163–179 (February 2001)
Clarke, M.E., Grumberg, O. and Peled, D.A.: Model Checking. MIT Press (1999, 2nd printing 2000)
Cribbens, A.H.: Solid State Interlocking (SSI): an Integrated Electronic Signalling System for Mainline Railways. IEE Proceedings, Part B: Electric Power Applications, Volume 134, Issue 3, pp148–158. IEE (1987)
Cribbens, A.H. and Mitchell, I.H.: The Application of Advanced Computing Techniques to the Generation and Checking of SSI Data. Institution of Railway Signal Engineers. IRSE Proceedings, Volume 1991/92, pp 54–64 (1991)
Gurukumba, T.: From GDL to CSP: towards the full formal verification of solid state interlockings. Oxford University, MSc dissertation (1998)
Huber, M.: Towards an Industrially Applicable Model Checker for Railway Signalling Data. York University, MSc Dissertation, Department of Computer Science (2001)
Leach, M. (ed.): Railway Control Systems. Institution of Railway Signal Engineers. A & C Black, London (1991, Reprint 1993)
McMillan, K.L.: Symbolic Model Checking. Carnegie Mellon University, PhD thesis CMU-CS-92-131 (1992)
Morley, M.J.: Safety Assurance in Interlocking Design. Edinburgh University, PhD thesis ECS-LFCS-96-348 (1996)
Morley, M.J.: Semantics of Geographic Data Languages. In Proceedings of the 1st FMERail Workshop; Breukelen, Netherlands (June 1998)
Raili, E.L.: The Verification of the Design of Railway Networks. York University, MSc Dissertation, Department of Computer Science (1996)
Simpson, A.: Model Checking for Interlocking Safety. In Proceedings of the 2nd FMERail Workshop, Canary Wharf, London (October 1998)
SSI 8003: SSI Applications Manual. London: Railtrack, Head of Corporate Standards, electronic copy (February 1999)
Westerman, S.J., Shryane, N.M., and Sauer, J.: Task Analysis of the Solid State Interlocking Design Process. Human Factors in the Design of Safety Critical Systems project, Work package 1.1, Report No. SCS-01. University of Hull, Department of Psychology (April 1994)
Westerman, S.J., Shryane, N.M., Crawshaw, C.M. and Hockey, G.R.J.: Error Analysis of the Solid State Interlocking Design Process. Human Factors in the Design of Safety Critical Systems project, Work package 1.2, Report No. SCS-04. University of Hull, Department of Psychology (June 1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Huber, M., King, S. (2002). Towards an Integrated Model Checker for Railway Signalling Data. In: Eriksson, LH., Lindsay, P.A. (eds) FME 2002:Formal Methods—Getting IT Right. FME 2002. Lecture Notes in Computer Science, vol 2391. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45614-7_12
Download citation
DOI: https://doi.org/10.1007/3-540-45614-7_12
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43928-8
Online ISBN: 978-3-540-45614-8
eBook Packages: Springer Book Archive