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
Country/TerritoryUnited States
CityMoffett Field
Period16/05/201718/05/2017
SeriesLecture Notes in Computer Science
Volume10227
ISSN0302-9743

Keywords

  • Railway interlocking
  • Compositional verification
  • Model checking

Fingerprint

Dive into the research topics of 'Compositional Model Checking of Interlocking Systems for Lines with Multiple Stations'. Together they form a unique fingerprint.

Cite this