Author(s)

CYDNEY MINKOWITZ

Abstract

The Smartlock 400 (SML400) SSI-based interlocking product is one of a family of Alstom’s railway interlocking products which was developed as a replacement for the Solid State Interlocking (SSI) product. A software tool has been introduced in the SML400 application engineering process to validate the application data against safety conditions, or rather to prove that the application data does not violate specified constraint violations. The aims when designing the tool were to: develop customized software based on a model of the application data generated by existing tools (rather than use a generic theorem prover, to avoid having to translate the data into another notation); use a dynamic technique similar to symbolic execution (as the nature of the data renders it difficult to use static model checking techniques); and employ application specific rules to make the technique manageable (i.e. to reduce the search space of proofs). The tool has demonstrated good performance on average sized and large interlocking applications. By customer request, it has been used principally to validate points free-to-move (PFM) conditions; it has found known data errors caused by points being commanded without having been tested free to move, imprecise definitions of PFM conditions and incomplete PFM tests across interlocking boundaries. The paper begins with the motivation behind the tool’s introduction. It describes the context of the tool, including the characteristics of the application data, the way in which constraint violations are expressed and the operations performed by the tool. It contains descriptions of sample rules used by the tool to optimise the proofs. It compares the tool with other tools that have been used to verify safety properties of SSI-based data. The paper ends by proposing further work for the enhancement and use of the tool.

Keywords

railway interlocking systems, SSI, safety-critical systems, model-based reasoning, formal methods, VDM++