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.
Model Checking Geographically Distributed Interlocking Systems Using UMC / Fantechi, Alessandro; Haxthausen, Anne E.; Nielsen, Michel Boje Randahl. - STAMPA. - (2017), pp. 278-286. (Intervento presentato al convegno 25th Euromicro International Conference on Parallel, Distributed and Network-Based Processing, PDP 2017 tenutosi a rus nel 2017) [10.1109/PDP.2017.66].
Model Checking Geographically Distributed Interlocking Systems Using UMC
Fantechi, Alessandro;
2017
Abstract
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.I documenti in FLORE sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.