Formal Verification of the Danish Railway Interlocking Systems

Linh Hong Vu, Anne Elisabeth Haxthausen, Jan Peleska

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

192 Downloads (Pure)

Abstract

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
Publication statusPublished - 2014
Event14th International Workshop on Automated Verification of Critical Systems, AVoCS 2014 - University of Twente, Enschede, Netherlands
Duration: 24 Sep 201426 Sep 2014
Conference number: 14
http://fmt.cs.utwente.nl/conferences/avocs2014/

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

Cite this

Vu, L. H., Haxthausen, A. E., & Peleska, J. (2014). Formal Verification of the Danish Railway Interlocking Systems. In M. Huisman, & J. van de Pol (Eds.), Pre-proceedings of 14th International Workshop on Automated Verification of Critical Systems (AVoCS 2014) (pp. 257-258). University of Twente. C T I T Workshop Proceedings Series, No. WP 14-01 http://fmt.cs.utwente.nl/conferences/avocs2014/AVoCS2014Proceedings.pdf