Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
|
 |
Model Checking Safety Critical Software with SPIN: an Application to a Railway Interlocking System
| |
|
Model Checking Safety Critical Software with SPIN: an Application to a Railway Interlocking System
Alessandro Cimatti5, Fausto Giunchiglia5, Giorgio Mongardi6, Dario Romano6, Fernando Torielli6 and Paolo Traverso5
| (5) |
Istituto per la Ricerca Scientifica e Tecnologica (IRST), 38050 Povo, Trento, Italy |
| (6) |
Ansaldo Segnalamento Ferroviario (ASF), Via dei Pescatori 35, 16129 Genova, Italy |
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.
Fulltext Preview (Small, Large)
 References secured to subscribers.
|
|
|
|
|
|