Modelling and Verification of Relay Interlocking Systems

Anne Elisabeth Haxthausen (Invited author), Marie Le Bliguet (Invited author), Andreas Kjær (Invited author)

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

1 Downloads (Pure)

Abstract

This paper describes how relay interlocking systems as used by the Danish railways can be formally modelled and verified. Such systems are documented by circuit diagrams describing their static layout. It is explained how to derive a state transition system model for the dynamic behaviour of a relay system from such diagrams. Safety properties are identified and formalised as LTL formulae. Model checking is finally used to verify that a model satisfies the safety properties. The method is tested for an existing station in Denmark.
Original languageEnglish
Title of host publicationFoundations of Computer Software : Future Trends and Techniques for Development.
EditorsChristine Choppy, Oleg Sokolsky
Number of pages275
PublisherSpringer
Publication date2010
Pages141-153
ISBN (Print)978-3-642-12565-2
DOIs
Publication statusPublished - 2010
Event15th Monterey Workshop - Budapest, Hungary
Duration: 1 Jan 2008 → …

Conference

Conference15th Monterey Workshop
CityBudapest, Hungary
Period01/01/2008 → …
SeriesLecture Notes in Computer Science
Number6028

Bibliographical note

Invited paper.

Keywords

  • relay interlocking systems
  • formal methods
  • verification
  • railway control systems
  • software engineering

Cite this

Haxthausen, A. E., Bliguet, M. L., & Kjær, A. (2010). Modelling and Verification of Relay Interlocking Systems. In C. Choppy, & O. Sokolsky (Eds.), Foundations of Computer Software: Future Trends and Techniques for Development. (pp. 141-153). Springer. Lecture Notes in Computer Science, No. 6028 https://doi.org/10.1007/978-3-642-12566-9_8