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)


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
Publication date2017
ISBN (Print)978-3-319-57287-1
ISBN (Electronic)978-3-319-57288-8
Publication statusPublished - 2017
EventNASA Formal Methods Symposium 2017 - Moffett Field, United States
Duration: 16 May 201718 May 2017


ConferenceNASA Formal Methods Symposium 2017
CountryUnited States
CityMoffett Field
SeriesLecture Notes in Computer Science


  • 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