Compositional Model Checking of Interlocking Systems for Lines with Multiple Stations

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedings – Annual report year: 2017Researchpeer-review

View graph of relations

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
CitationsWeb of Science® Times Cited: No match on DOI

    Research areas

  • Railway interlocking , Compositional verification, Model checking

ID: 133173701