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

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

Cimatti, Alessandro;Giunchiglia, Fausto;Traverso, Paolo
1998-01-01

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 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
1998
9783540651109
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11582/1732
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
social impact