Compositional Model Checking of Interlocking Systems for Lines with Multiple Stations

Publication: Research - peer-reviewArticle in proceedings – Annual report year: 2017

DOI

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
PublisherSpringer
Publication date2017
Pages146–162
DOIs
StatePublished - 2017
EventNASA Formal Methods Symposium 2017 - Moffett Field, United States

Conference

ConferenceNASA Formal Methods Symposium 2017
CountryUnited States
CityMoffett Field
Period16/05/201718/05/2017
SeriesLecture Notes in Computer Science
Volume10227
ISSN0302-9743
CitationsWeb of Science® Times Cited: No match on DOI

    Keywords

  • Railway interlocking , Compositional verification, Model checking
Download as:
Download as PDF
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
PDF
Download as HTML
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
HTML
Download as Word
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
Word

ID: 133173701