PT Unknown
AU Dipoppa, G
   D'Alessandro, G
   Semprini, R
   Tronci, E
TI Integrating Automatic Verification of Safety Requirements in Railway Interlocking System Design
SE High Assurance Systems Engineering, 2001. Sixth IEEE International Symposium on
PY 2001
BP 209
EP 219
DI 10.1109/HASE.2001.966821
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.
PI Albuquerque, NM, USA
ER