A formal verification environment for railway signalling system design

An experience is reported OIl the specificatiou and verification of safety requirements of a railway interlocking system using formal methods. A model theoretical approach has been used for both the specification and the proof of the safety properties of the system. We used the JACK environment which integrates a set of verification tools, supported by a graphical interface offering facilities to use these tools separately or in combination. The experiment carried out has shown that the methodology can be applied successfully in the verification of industrial safety critical systems.