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.
Formal Modeling and Verification of Interlocking Systems Featuring Sequential Release
Communic.Comp.Inf.Science
International Workshop on Formal Techniques for Safety-Critical Systems ; 2014 ; Luxembourg, Luxembourg November 6, 2014 - November 7, 2014
2015-04-16
16 pages
Article/Chapter (Book)
Electronic Resource
English
Comparing Formal Verification Approaches of Interlocking Systems
British Library Conference Proceedings | 2016
|Interlocking Formal Verification at Alstom Signalling
British Library Conference Proceedings | 2019
|Formal Methods for Industrial Interlocking Verification
IEEE | 2018
|Principles of formal verification of interlocking software
Tema Archive | 2007
|Validation of Railway Interlocking Systems by Formal Verification, A Case Study
British Library Conference Proceedings | 2014
|