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

This paper reports on an experience in formal verification using SPIN. The analyzed system is the Safety Logic of an interlocking system for the control of railway 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. In this paper we describe how a PROMELA model has been devised, which retains the configurability features of this architecture. Furthermore, we discuss the verification with SPIN of significant process configurations