%0 Conference Proceedings
%T Integrating Automatic Verification of Safety Requirements in Railway Interlocking System Design
%A Dipoppa, G.
%A D'Alessandro, G.
%A Semprini, R.
%A Tronci, E.
%S High Assurance Systems Engineering, 2001. Sixth IEEE International Symposium on
%D 2001
%I IEEE Computer Society
%C Albuquerque, NM, USA
%@ 0-7695-1275-5
%F Dipoppa_etal2001
%O exported from refbase (http://mclab.di.uniroma1.it/publications/show.php?record=45), last updated on Sat, 24 Nov 2012 14:30:10 +0100
%X 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.
%R 10.1109/HASE.2001.966821
%U http://mclab.di.uniroma1.it/publications/papers/papers/Dipoppa2001.pdf
%U https://doi.org/10.1109/HASE.2001.966821
%P 209-219