Model Checking Safety Critical Software with SPIN: An Application to a Railway Interlocking System

This paper describes an industrial application in formal verification. The analyzed system is the Safety Logic of an interlocking system for the control of railways stations developed by Ansaldo. The Safety Logic is a process-based software architecture, which can be configured to implement different functions and control stations of different topology. The applied technique, model checking, allows for the representation of the analyzed system as a finite state machines. Specialized algorithms allow for the automatic and efficient verification of requirements by means of an exhaustive exploration of the state space. In this paper we describe how a formal model of the Safety Logic has been developed in the language of the SPIN model checker. This model retains the configurability features of the Safety Logic. Furthermore, we discuss how the automated verification of several significant process configuration was carried out without incurring into the state explosion problem