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
Model Checking Safety Critical Software with SPIN: An Application to a Railway Interlocking System
Cimatti, Alessandro;Giunchiglia, Fausto;Traverso, Paolo
1997-01-01
Abstract
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 configurationsFile 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.