Conference:

Sixth IEEE International Symposium on
High Assurance Systems Engineering (HASE)
22-24 October 2001, Boca Raton, Florida, USA,


Paper Title:

Integrating Automatic Verification of Safety Requirements 
in Railway Interlocking System Design


Keywords:

Model Checking, Automatic Verification, Bounded Model Chekcing,
Formal Methods, Railway Interlocking Systems.



Authors and Affiliations:

Giovanni Dipoppa
ENEA C.R.-CASACCIA, TISGI Section,
Via Anguillarese, 301,  
S.Maria di Galeria I-00060 ROMA - ITALY, 
email: giovanni.dipoppa@casaccia.enea.it
url: http://tisgi.casaccia.enea.it 

Giovanni D'Alessandro
CASPUR, c/o CICS Universita' di Roma ``La Sapienza'', 
Piazzale Aldo Moro 5, I-00185, 
Roma - ITALY
email: Giovanni.Dalessandro@caspur.it


Roberto Semprini
System Assurance,
ALSTOM TRANSPORT SpA, 
Via di Corticella 75,
I-40128  Bologna - ITALY 
email: roberto.semprini@transport.alstom.com
url: http://www.alstom.com

Enrico Tronci
Area Informatica,
Universit\`a di L'Aquila, 
Coppito I-67100 L'Aquila - ITALY 
email: tronci@univaq.it
url: http://univaq.it/~tronci 



Abstract

A {\em Railway Interlocking System} (RIS) is an Embedded System 
(namely a Supervisory Control System) that
ensures the safe operation of the devices in a Railway Station.
Of course a RIS is a {\em Safety Critical System}.


In this paper we explore the
possibility of integrating automatic formal verification
methods in a given industry  RIS design flow.

The main obstructions to be overcome in our work 
are: selecting a formal verification tool that is 
efficient enough to solve the 
verification problems at hand and  devising a
cost effective integration strategy for such tool.

Eventually we were able to devise a successful
integration strategy meeting the above 
constraints.
This is done without requiring major
modification in the preexistent design flow nor 
retraining of personnel.


We run verification experiments for a RIS designed 
for the Singapore Subway. Such experiments show
that the RIS design flow obtained from our integration strategy
will indeed be able to automatically verify 
{\em real life} RIS designs.