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 language | English |
|---|---|
| Title of host publication | Pre-proceedings of 14th International Workshop on Automated Verification of Critical Systems (AVoCS 2014) |
| Editors | Marieke Huisman, Jaco van de Pol |
| Publisher | University of Twente |
| Publication date | 2014 |
| Pages | 257-258 |
| Publication status | Published - 2014 |
| Event | 14th International Workshop on Automated Verification of Critical Systems, AVoCS 2014 - University of Twente, Enschede, Netherlands Duration: 24 Sept 2014 → 26 Sept 2014 Conference number: 14 http://fmt.cs.utwente.nl/conferences/avocs2014/ |
Workshop
| Workshop | 14th International Workshop on Automated Verification of Critical Systems, AVoCS 2014 |
|---|---|
| Number | 14 |
| Location | University of Twente |
| Country/Territory | Netherlands |
| City | Enschede |
| Period | 24/09/2014 → 26/09/2014 |
| Internet address |
| Series | C T I T Workshop Proceedings Series |
|---|---|
| Number | WP 14-01 |
| ISSN | 1574-0846 |
Keywords
- railway interlocking systems
- formal verification
- bounded model checking
- k-induction
- safety-critical software systems
- RobustRails