Name
Abstract | ||
|---|---|---|
The safety analysis of interlocking railway systems involves verifying collision and derailment freedom. In this paper we propose a structured way of refining track plans, in order to expand track segments so that they form collections of track segments. We show how the abstract model can be model checked to ensure the safety properties, which must also hold in the corresponding concrete track plan, so that we will never need to model check the concrete track plan directly. We also identify the minimal number of trains that needs to be considered as part of the model checking, and we demonstrate the practicality of the approach on various scenarios. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1007/978-3-642-39611-3_20 | Haifa Verification Conference |
Keywords | Field | DocType |
refining track plan,model checking,abstract model,interlocking railway system,safety analysis,track segment,model checking abstraction,safety property,concrete track plan,derailment freedom,complex railway model,corresponding concrete track plan | Abstraction,Model checking,Interlocking,Software engineering,Simulation,Computer science,Derailment,Collision,Theoretical computer science,Control table,Proof obligation,Train | Conference |
Citations | PageRank | References |
8 | 0.63 | 9 |
Authors | ||
5 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Faron Moller | 1 | 1336 | 110.75 |
| Hoang Nga Nguyen | 2 | 80 | 12.80 |
| Markus Roggenbach | 3 | 294 | 32.63 |
| Steve Schneider | 4 | 1425 | 116.55 |
| Helen Treharne | 5 | 390 | 36.94 |