Formal Modeling and Verification of Interlocking Systems Featuring Sequential Release

Publication: Research - peer-reviewArticle in proceedings – Annual report year: 2014

View graph of relations

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
StatePublished - 2014
EventThird International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2014) - Luxembourg, Luxembourg

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
Download as:
Download as PDF
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
PDF
Download as HTML
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
HTML
Download as Word
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
Word

Download statistics

No data available

ID: 102205125