Formal modelling and verification of interlocking systems featuring sequential release

Linh Hong Vu, Anne Elisabeth Haxthausen, Jan Peleska

Research output: Contribution to journalJournal articleResearchpeer-review

334 Downloads (Pure)


In this article, we present a method and an associated toolchain for the formal verification of the new Danish railway interlocking systems that are compatible with the European Train Control System (ETCS) Level 2. We have made a generic and reconfigurable model of the system behaviour and generic safety properties. This model accommodates sequential release - a feature in the new Danish interlocking systems. To verify the safety of an interlocking system, first a domain-specific description of interlocking configuration data is constructed and validated. Then the generic model and safety properties are automatically instantiated with the well-formed description of interlocking configuration data. This instantiation produces a model instance in the form of a Kripke structure, and concrete safety properties expressed as invariants. Finally, using a combination of SMT based bounded model checking (BMC) and inductive reasoning, it is verified that the generated model instance satisfies the generated safety properties. Using this method, we are able to verify the safety properties for model instances corresponding to railway networks of industrial size. Experiments show that BMC is also efficient for finding bugs in the railway interlocking designs. Additionally, benchmarking results comparing the performance of our approach with alternative verification techniques on the interlocking models are presented.
Original languageEnglish
JournalScience of Computer Programming
Pages (from-to)91-115
Publication statusPublished - 2017


  • Railway interlocking systems
  • Sequential release
  • Formal verification
  • Bounded model checking
  • k-Induction


Dive into the research topics of 'Formal modelling and verification of interlocking systems featuring sequential release'. Together they form a unique fingerprint.

Cite this