@InProceedings{Dipoppa_etal2001,
author="Dipoppa, G.
and D{\textquoteright}Alessandro, G.
and Semprini, R.
and Tronci, E.",
title="Integrating Automatic Verification of Safety Requirements in Railway Interlocking System Design",
booktitle="High Assurance Systems Engineering, 2001. Sixth IEEE International Symposium on",
year="2001",
publisher="IEEE Computer Society",
address="Albuquerque, NM, USA",
pages="209--219",
abstract="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.",
optnote="exported from refbase (http://mclab.di.uniroma1.it/publications/show.php?record=45), last updated on Sat, 24 Nov 2012 14:30:10 +0100",
issn="0-7695-1275-5",
doi="10.1109/HASE.2001.966821",
opturl="https://doi.org/10.1109/HASE.2001.966821",
file=":http://mclab.di.uniroma1.it/publications/papers/papers/Dipoppa2001.pdf:PDF"
}