Towards an integrated model checker for railway signalling data

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.