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

439 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 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
Publication statusPublished - 2015
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
SeriesCommunications in Computer and Information Science
Volume476
ISSN1865-0929

Keywords

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

Cite this

Vu, L. H., Haxthausen, A. E., & Peleska, J. (2015). Formal Modeling and Verification of Interlocking Systems Featuring Sequential Release. In C. Artho, & P. Csaba Ölveczky (Eds.), Proceedings of the 3rd International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2014) (pp. 223-238). Springer. Communications in Computer and Information Science, Vol.. 476 https://doi.org/10.1007/978-3-319-17581-2_15