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)


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
Publication date2010
ISBN (Print)978-3-642-12565-2
Publication statusPublished - 2010
Event15th Monterey Workshop - Budapest, Hungary
Duration: 1 Jan 2008 → …


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

Bibliographical note

Invited paper.


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


Dive into the research topics of 'Modelling and Verification of Relay Interlocking Systems'. Together they form a unique fingerprint.

Cite this