Model Checking Geographically Distributed Interlocking Systems Using UMC
Alessandro Fantechi, Anne E. Haxthausen, Michel Boje Randahl Nielsen · 2017
The current trend of distributing computations over a network is here, as a novelty, applied to a safety critical system, namely a railway interlocking system. We show how the challenge of guaranteeing safety of the distributed application has been attacked by formally specifying and model checking the relevant distributed protocols. By doing that we obey the safety guidelines of the railway signalling domain, that require formal methods to support the certification of such products. We also show how formal modelling can help designing alternative distributed solutions, while maintaining adherence to safety constraints.