Validation of a railway interlocking model

Abstract

This paper presents a VDM model of a real-life railway interlocking system, and describes how this model is validated through simulation in ML. The model development illustrates how concepts may be captured for a non-trivial system. The steps from a predicative VDM model to an executable ML program are also outlined. The importance of validation by simulation is highlighted by giving two equally plausible safety requirements for the system and the end users reaction to the simulation. For safety reasons, we find it important that the model also can form the basis for formal program development, where the correctness of the program with respect to the specification can be formally verified. Therefore we advocate to make a model which can be used for simulation as well as formal program development.