TY  - CONF
AU  - Dipoppa, G.
AU  - D'Alessandro, G.
AU  - Semprini, R.
AU  - Tronci, E.
PY  - 2001
DA  - 2001//
TI  - Integrating Automatic Verification of Safety Requirements in Railway Interlocking System Design
BT  - High Assurance Systems Engineering, 2001. Sixth IEEE International Symposium on
SP  - 209
EP  - 219
PB  - IEEE Computer Society
CY  - Albuquerque, NM, USA
AB  - A 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. RIS is a safety critical system. 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. We were able to devise a successful integration strategy meeting the above constraints without requiring major modification in the pre-existent design flow nor retraining of personnel. We run verification experiments for a RIS designed for the Singapore Subway. The experiments show that the RIS design flow obtained from our integration strategy is able to automatically verify real life RIS designs.
SN  - 0-7695-1275-5
L1  - http://mclab.di.uniroma1.it/publications/papers/papers/Dipoppa2001.pdf
UR  - https://doi.org/10.1109/HASE.2001.966821
DO  - 10.1109/HASE.2001.966821
N1  - exported from refbase (http://mclab.di.uniroma1.it/publications/show.php?record=45), last updated on Sat, 24 Nov 2012 14:30:10 +0100
ID  - Dipoppa_etal2001
ER  -