Formal Modeling and Verification of Interlocking Systems Featuring Sequential Release

Linh Hong Vu, Anne Elisabeth Haxthausen, Jan Peleska

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

691 Downloads (Pure)

Abstract

In this paper, we present a method and an associated tool suite for formal verification of the new ETCS level 2 based Danish railway interlocking systems. We have made a generic and reconfigurable model of the system behavior and generic high-level safety properties. This model accommodates sequential release - a feature in the new Danish interlocking systems. The generic model and safety properties can be instantiated with interlocking configuration data, resulting in a concrete model in the form of a Kripke structure, and in high-level safety properties expressed as state invariants. Using SMT based bounded model checking (BMC) and inductive reasoning, we are able to verify the properties for model instances corresponding to railway networks of industrial size. Experiments also show that BMC is efficient for finding bugs in the railway interlocking designs.
Original languageEnglish
Title of host publicationPreliminary Proceedings of the Third International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2014)
EditorsCyrille Artho, Peter Csaba Ölveczky
Publication date2014
Pages58-73
Publication statusPublished - 2014
EventThird International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2014) - Luxembourg, Luxembourg
Duration: 3 Nov 20147 Nov 2014
Conference number: 3
http://www.ftscs.org/

Workshop

WorkshopThird International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2014)
Number3
CountryLuxembourg
CityLuxembourg
Period03/11/201407/11/2014
OtherA satellite event of the ICFEM 2014 conference.
Internet address

Bibliographical note

Revised versions of accepted regular papers will appear in the post-proceedings of FTSCS 2014 that will be published as a volume in Springer’s Communications in Computer and Information Science (CCIS) series.

Keywords

  • Railway interlocking systems
  • Formal verification
  • Bounded model checking
  • Inductive reasoning
  • Robust Rails
  • Safety-critical systems

Fingerprint Dive into the research topics of 'Formal Modeling and Verification of Interlocking Systems Featuring Sequential Release'. Together they form a unique fingerprint.

Cite this