Formal Verification of the Danish Railway Interlocking Systems

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

View graph of relations

In this paper, we present a method for formal verification of the new Danish railway interlocking systems. We made a generic and reconfigurable model of the behaviors and high-level safety properties of non-collision and nonderailment. This model accommodates sequential release – a new feature in the new Danish interlocking systems. Instantiating the generic model with interlocking configuration data results in a concrete model and high-level safety properties. Using bounded model checking and inductive reasoning, we are able to verify safety properties for model instances corresponding to railway networks of industrial size.
Original languageEnglish
Title of host publicationPre-proceedings of 14th International Workshop on Automated Verification of Critical Systems (AVoCS 2014)
EditorsMarieke Huisman, Jaco van de Pol
PublisherUniversity of Twente
Publication date2014
Pages257-258
StatePublished - 2014
Event14th International Workshop on Automated Verification of Critical Systems, AVoCS 2014 - Enschede, Netherlands

Workshop

Workshop14th International Workshop on Automated Verification of Critical Systems, AVoCS 2014
Number14
LocationUniversity of Twente
CountryNetherlands
CityEnschede
Period24/09/201426/09/2014
Internet address
SeriesC T I T Workshop Proceedings Series
NumberWP 14-01
ISSN1574-0846

    Keywords

  • railway interlocking systems, formal verification, bounded model checking, k-induction, safety-critical software systems, RobustRails
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: 102282363