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

This paper describes how a formal model of the Safety Logic has been develped in the language of the spin model checker and discusses how the automated verification of several significant process configurations was carried out without incurring into the state explosion problem.

Abstract

This paper describes an industrial application in formal verification. 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 difierent functions and control stations of difierent 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 eficient 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 develped 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 configurations was carried out without incurring into the state explosion problem.