An experience in formal verification of safety properties of a railway signalling control system

An experience on the specification and verification of a railway interlocking system produced in a joint project with Ansaldo and the Italian Railways is reported. In the project we have used the JACK environment both to build the algebraic and graphical specification of such a system and to perform the verification of logic formulae on the model of the system itself. JACK is an environment integrating a set of verification tools, supported by a graphical interface offering facilities to use these tools separately or in combination. The experiment carried on has shown that the methodology can be applied successfully in the verification of safety critical systems. 1