Verification of railway interlocking systems

Simon Busard
(Université catholique de Louvain)
Quentin Cappart
(Université catholique de Louvain)
Christophe Limbrée
(Université catholique de Louvain)
Charles Pecheur
(Université catholique de Louvain)
Pierre Schaus
(Université catholique de Louvain)

In the railway domain, an interlocking is a computerised system that controls the railway signalling objects in order to allow a safe operation of the train traffic. Each interlocking makes use of particular data, called application data, that reflects the track layout of the station under control. The verification and validation of the application data are performed manually and is thus error-prone and costly. In this paper, we explain how we built an executable model in NuSMV of a railway interlocking based on the application data. We also detail the tool that we have developed in order to translate the application data into our model automatically. Finally we show how we could verify a realistic set of safety properties on a real-size station model by customizing the existing model-checking algorithm with PyNuSMV a Python library based on NuSMV.

In Jun Pang, Yang Liu and Sjouke Mauw: Proceedings 4th International Workshop on Engineering Safety and Security Systems (ESSS 2015), Oslo, Norway, June 22, 2015, Electronic Proceedings in Theoretical Computer Science 184, pp. 19–31.
Published: 10th June 2015.

ArXived at: http://dx.doi.org/10.4204/EPTCS.184.2 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org