Book chapter · Conference paper
Formal Modeling and Verification of Interlocking Systems Featuring Sequential Release
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.
| Language: | English |
|---|---|
| Publisher: | Springer |
| Year: | 2015 |
| Pages: | 223-238 |
| Proceedings: | Third International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2014)International Workshop on Formal Techniques for Safety-Critical Systems |
| Series: | Communications in Computer and Information Science |
| ISBN: | 3319175807 , 3319175815 , 9783319175805 and 9783319175812 |
| ISSN: | 18650937 and 18650929 |
| Types: | Book chapter and Conference paper |
| DOI: | 10.1007/978-3-319-17581-2_15 |
| ORCIDs: | Haxthausen, Anne Elisabeth |
