Formal Modeling and Verification of Interlocking Systems Featuring Sequential Release

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

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 publicationProceedings of the 3rd International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2014)
EditorsCyrille Artho, Peter Csaba Ölveczky
PublisherSpringer
Publication date2015
Pages223-238
ISBN (print)978-3-319-17580-5
ISBN (electronic) 978-3-319-17581-2
DOIs
StatePublished - 2015
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
SeriesCommunications in Computer and Information Science
Volume476
ISSN1865-0929
CitationsWeb of Science® Times Cited: 8

    Keywords

  • Railway interlocking systems, Formal verification, Bounded model checking, Inductive reasoning, RobustRails, 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: 118946810