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

161 Downloads (Pure)

Abstract

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
Volume133
Pages (from-to)91-115
ISSN0167-6423
DOIs
Publication statusPublished - 2017

Keywords

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

Cite this

@article{c9dd8de22ecf416699eff076b6fa61a5,
title = "Formal modelling and verification of interlocking systems featuring sequential release",
abstract = "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.",
keywords = "Railway interlocking systems, Sequential release, Formal verification, Bounded model checking, k-Induction",
author = "Vu, {Linh Hong} and Haxthausen, {Anne Elisabeth} and Jan Peleska",
year = "2017",
doi = "10.1016/j.scico.2016.05.010",
language = "English",
volume = "133",
pages = "91--115",
journal = "Science of Computer Programming",
issn = "0167-6423",
publisher = "Elsevier",

}

Formal modelling and verification of interlocking systems featuring sequential release. / Vu, Linh Hong; Haxthausen, Anne Elisabeth; Peleska, Jan.

In: Science of Computer Programming, Vol. 133, 2017, p. 91-115.

Research output: Contribution to journalJournal articleResearchpeer-review

TY - JOUR

T1 - Formal modelling and verification of interlocking systems featuring sequential release

AU - Vu, Linh Hong

AU - Haxthausen, Anne Elisabeth

AU - Peleska, Jan

PY - 2017

Y1 - 2017

N2 - 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.

AB - 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.

KW - Railway interlocking systems

KW - Sequential release

KW - Formal verification

KW - Bounded model checking

KW - k-Induction

U2 - 10.1016/j.scico.2016.05.010

DO - 10.1016/j.scico.2016.05.010

M3 - Journal article

VL - 133

SP - 91

EP - 115

JO - Science of Computer Programming

JF - Science of Computer Programming

SN - 0167-6423

ER -