Compositional Model Checking of Interlocking Systems for Lines with Multiple Stations

Hugo Daniel dos Santos Macedo, Alessandro Fantechi, Anne Elisabeth Haxthausen

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

1 Downloads (Pure)

Abstract

In the railway domain safety is guaranteed by an interlocking system which translates operational decisions into commands leading to field operations. Such a system is safety critical and demands thorough formal verification during its development process. Within this context, our work has focused on the extension of a compositional model checking approach to formally verify interlocking system models for lines with multiple stations. The idea of the approach is to decompose a model of the interlocking system by applying cuts at the network modelling level. The paper introduces an alternative cut (the linear cut) to a previously proposed cut (border cut). Powered with the linear cut, the model checking approach is then applied to the verification of an interlocking system controlling a real-world multiple station line.
Original languageEnglish
Title of host publicationProceedings of NASA Formal Methods Symposium 2017
PublisherSpringer
Publication date2017
Pages146–162
ISBN (Print)978-3-319-57287-1
ISBN (Electronic)978-3-319-57288-8
DOIs
Publication statusPublished - 2017
EventNASA Formal Methods Symposium 2017 - Moffett Field, United States
Duration: 16 May 201718 May 2017

Conference

ConferenceNASA Formal Methods Symposium 2017
CountryUnited States
CityMoffett Field
Period16/05/201718/05/2017
SeriesLecture Notes in Computer Science
Volume10227
ISSN0302-9743

Keywords

  • Railway interlocking
  • Compositional verification
  • Model checking

Cite this

Macedo, H. D. D. S., Fantechi, A., & Haxthausen, A. E. (2017). Compositional Model Checking of Interlocking Systems for Lines with Multiple Stations. In Proceedings of NASA Formal Methods Symposium 2017 (pp. 146–162). Springer. Lecture Notes in Computer Science, Vol.. 10227 https://doi.org/10.1007/978-3-319-57288-8_11
Macedo, Hugo Daniel dos Santos ; Fantechi, Alessandro ; Haxthausen, Anne Elisabeth. / Compositional Model Checking of Interlocking Systems for Lines with Multiple Stations. Proceedings of NASA Formal Methods Symposium 2017. Springer, 2017. pp. 146–162 (Lecture Notes in Computer Science, Vol. 10227).
@inproceedings{73244fbe25584ca8af9a2a67b4d00a92,
title = "Compositional Model Checking of Interlocking Systems for Lines with Multiple Stations",
abstract = "In the railway domain safety is guaranteed by an interlocking system which translates operational decisions into commands leading to field operations. Such a system is safety critical and demands thorough formal verification during its development process. Within this context, our work has focused on the extension of a compositional model checking approach to formally verify interlocking system models for lines with multiple stations. The idea of the approach is to decompose a model of the interlocking system by applying cuts at the network modelling level. The paper introduces an alternative cut (the linear cut) to a previously proposed cut (border cut). Powered with the linear cut, the model checking approach is then applied to the verification of an interlocking system controlling a real-world multiple station line.",
keywords = "Railway interlocking , Compositional verification, Model checking",
author = "Macedo, {Hugo Daniel dos Santos} and Alessandro Fantechi and Haxthausen, {Anne Elisabeth}",
year = "2017",
doi = "10.1007/978-3-319-57288-8_11",
language = "English",
isbn = "978-3-319-57287-1",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "146–162",
booktitle = "Proceedings of NASA Formal Methods Symposium 2017",

}

Macedo, HDDS, Fantechi, A & Haxthausen, AE 2017, Compositional Model Checking of Interlocking Systems for Lines with Multiple Stations. in Proceedings of NASA Formal Methods Symposium 2017. Springer, Lecture Notes in Computer Science, vol. 10227, pp. 146–162, NASA Formal Methods Symposium 2017, Moffett Field, United States, 16/05/2017. https://doi.org/10.1007/978-3-319-57288-8_11

Compositional Model Checking of Interlocking Systems for Lines with Multiple Stations. / Macedo, Hugo Daniel dos Santos; Fantechi, Alessandro; Haxthausen, Anne Elisabeth.

Proceedings of NASA Formal Methods Symposium 2017. Springer, 2017. p. 146–162 (Lecture Notes in Computer Science, Vol. 10227).

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

TY - GEN

T1 - Compositional Model Checking of Interlocking Systems for Lines with Multiple Stations

AU - Macedo, Hugo Daniel dos Santos

AU - Fantechi, Alessandro

AU - Haxthausen, Anne Elisabeth

PY - 2017

Y1 - 2017

N2 - In the railway domain safety is guaranteed by an interlocking system which translates operational decisions into commands leading to field operations. Such a system is safety critical and demands thorough formal verification during its development process. Within this context, our work has focused on the extension of a compositional model checking approach to formally verify interlocking system models for lines with multiple stations. The idea of the approach is to decompose a model of the interlocking system by applying cuts at the network modelling level. The paper introduces an alternative cut (the linear cut) to a previously proposed cut (border cut). Powered with the linear cut, the model checking approach is then applied to the verification of an interlocking system controlling a real-world multiple station line.

AB - In the railway domain safety is guaranteed by an interlocking system which translates operational decisions into commands leading to field operations. Such a system is safety critical and demands thorough formal verification during its development process. Within this context, our work has focused on the extension of a compositional model checking approach to formally verify interlocking system models for lines with multiple stations. The idea of the approach is to decompose a model of the interlocking system by applying cuts at the network modelling level. The paper introduces an alternative cut (the linear cut) to a previously proposed cut (border cut). Powered with the linear cut, the model checking approach is then applied to the verification of an interlocking system controlling a real-world multiple station line.

KW - Railway interlocking

KW - Compositional verification

KW - Model checking

U2 - 10.1007/978-3-319-57288-8_11

DO - 10.1007/978-3-319-57288-8_11

M3 - Article in proceedings

SN - 978-3-319-57287-1

T3 - Lecture Notes in Computer Science

SP - 146

EP - 162

BT - Proceedings of NASA Formal Methods Symposium 2017

PB - Springer

ER -

Macedo HDDS, Fantechi A, Haxthausen AE. Compositional Model Checking of Interlocking Systems for Lines with Multiple Stations. In Proceedings of NASA Formal Methods Symposium 2017. Springer. 2017. p. 146–162. (Lecture Notes in Computer Science, Vol. 10227). https://doi.org/10.1007/978-3-319-57288-8_11