Model Checking Geographically Distributed Interlocking Systems Using UMC

Alessandro Fantechi, Anne Elisabeth Haxthausen, Michel Bøje Randahl Nielsen

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

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
Original languageEnglish
Title of host publication2017 25th Euromicro International Conference on Parallel, Distributed and Network-based Processing (PDP)
PublisherIEEE
Publication date2017
Pages278–286
DOIs
Publication statusPublished - 2017
Event2017 25th Euromicro International Conference on Parallel, Distributed and Network-based Processing - St. Petersburg, Russian Federation
Duration: 6 Mar 20178 Mar 2017

Conference

Conference2017 25th Euromicro International Conference on Parallel, Distributed and Network-based Processing
CountryRussian Federation
CitySt. Petersburg
Period06/03/201708/03/2017

Keywords

  • Model checking
  • Distributed systems
  • Railway interlocking systems

Cite this

Fantechi, A., Haxthausen, A. E., & Nielsen, M. B. R. (2017). Model Checking Geographically Distributed Interlocking Systems Using UMC. In 2017 25th Euromicro International Conference on Parallel, Distributed and Network-based Processing (PDP) (pp. 278–286). IEEE. https://doi.org/10.1109/PDP.2017.66
Fantechi, Alessandro ; Haxthausen, Anne Elisabeth ; Nielsen, Michel Bøje Randahl. / Model Checking Geographically Distributed Interlocking Systems Using UMC. 2017 25th Euromicro International Conference on Parallel, Distributed and Network-based Processing (PDP). IEEE, 2017. pp. 278–286
@inproceedings{301ed9d5620c412f9c0d8846e521ab67,
title = "Model Checking Geographically Distributed Interlocking Systems Using UMC",
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 showhow formal modelling can help designing alternative distributed solutions, while maintaining adherence to safety constraints",
keywords = "Model checking, Distributed systems, Railway interlocking systems",
author = "Alessandro Fantechi and Haxthausen, {Anne Elisabeth} and Nielsen, {Michel B{\o}je Randahl}",
year = "2017",
doi = "10.1109/PDP.2017.66",
language = "English",
pages = "278–286",
booktitle = "2017 25th Euromicro International Conference on Parallel, Distributed and Network-based Processing (PDP)",
publisher = "IEEE",
address = "United States",

}

Fantechi, A, Haxthausen, AE & Nielsen, MBR 2017, Model Checking Geographically Distributed Interlocking Systems Using UMC. in 2017 25th Euromicro International Conference on Parallel, Distributed and Network-based Processing (PDP). IEEE, pp. 278–286, 2017 25th Euromicro International Conference on Parallel, Distributed and Network-based Processing, St. Petersburg, Russian Federation, 06/03/2017. https://doi.org/10.1109/PDP.2017.66

Model Checking Geographically Distributed Interlocking Systems Using UMC. / Fantechi, Alessandro; Haxthausen, Anne Elisabeth; Nielsen, Michel Bøje Randahl.

2017 25th Euromicro International Conference on Parallel, Distributed and Network-based Processing (PDP). IEEE, 2017. p. 278–286.

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

TY - GEN

T1 - Model Checking Geographically Distributed Interlocking Systems Using UMC

AU - Fantechi, Alessandro

AU - Haxthausen, Anne Elisabeth

AU - Nielsen, Michel Bøje Randahl

PY - 2017

Y1 - 2017

N2 - 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 showhow formal modelling can help designing alternative distributed solutions, while maintaining adherence to safety constraints

AB - 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 showhow formal modelling can help designing alternative distributed solutions, while maintaining adherence to safety constraints

KW - Model checking

KW - Distributed systems

KW - Railway interlocking systems

U2 - 10.1109/PDP.2017.66

DO - 10.1109/PDP.2017.66

M3 - Article in proceedings

SP - 278

EP - 286

BT - 2017 25th Euromicro International Conference on Parallel, Distributed and Network-based Processing (PDP)

PB - IEEE

ER -

Fantechi A, Haxthausen AE, Nielsen MBR. Model Checking Geographically Distributed Interlocking Systems Using UMC. In 2017 25th Euromicro International Conference on Parallel, Distributed and Network-based Processing (PDP). IEEE. 2017. p. 278–286 https://doi.org/10.1109/PDP.2017.66