Modelling and Verification of Relay Interlocking Systems

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

View graph of relations

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.

CitationsWeb of Science® Times Cited: No match on DOI

    Research areas

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

ID: 5158951