Formal Verification of a Railway Interlocking System using Model Checking

In this paper we describe an industrial application of formal methods. We have used model checking techniques to model and formally verify a rather complex software, i.e. part of the “safety logic” of a railway interlocking system. The formal model is structured to retain the reusability and scalability properties of the system being modelled. Part of it is defined once for all at a low cost, and re-used. The rest of the model can be mechanically generated from the designers' current specification language. The model checker is “hidden” to the user, it runs as a powerful debugger. Its performances are impressive: exhaustive analysis of quite complex configurations with respect to rather complex properties are run in the order of minutes. The main reason for this achievement is essentially a carefully designed model, which exploits all the behaviour evolution constraints. The re-usability/scalability of the model and the fact that formal verification is automatic and efficient are the key factors which open up the possibility of a real usage by designers at design time. We have thus assessed the possibility of introducing the novel technique in the development cycle with an advantageous costs/benefits relation. Received March 1997 / Accepted in revised form July 1998