Conference paper
Formal Verification of the Danish Railway Interlocking Systems
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.
Language: | English |
---|---|
Publisher: | University of Twente |
Year: | 2014 |
Pages: | 257-258 |
Proceedings: | 14th International Workshop on Automated Verification of Critical Systems, AVoCS 2014 |
Series: | C T I T Workshop Proceedings Series |
ISSN: | 15740846 |
Types: | Conference paper |
ORCIDs: | Haxthausen, Anne Elisabeth |