A Framework for the Formal Verification of Networks of Railway Interlockings - Application to the Belgian Railway
- Title
- A Framework for the Formal Verification of Networks of Railway Interlockings - Application to the Belgian Railway
- Authors
- Christophe Limbrée?, Charles Pecheur
FM2018 Δ | 0Kb | 28 May 2020 |
Fmics2013 Δ | 0Kb | 28 May 2020 |
GandALF2017 Δ | 0Kb | 28 May 2020 |
HMI2011 Δ | 0Kb | 28 May 2020 |
LVLPrivate Δ | 0Kb | 28 May 2020 |
LVLPrivateNews Δ | 0Kb | 28 May 2020 |
Main Δ | 0Kb | 28 May 2020 |
Members Δ | 0Kb | 28 May 2020 |
Publications Δ | 4Kb | 28 May 2020 |
Site Δ | 0Kb | 28 May 2020 |
Talks Δ | 4Kb | 28 May 2020 |
Tools Δ | 0Kb | 28 May 2020 |
- Type
- In Proceedings
- Year
- 2018
Abstract
Modern railway stations are controlled by computerized systems called interlockings. In fact the middle size and large size stations usually require to use several interlockings, then forming a network of interlockings. Much research propose to verify the safety properties of such systems by means of model checking. Our approach goes a step further and proposes a method to extend the verification process to a network of interlockings. This process is known as compositional verification. Each interlocking is seen as the component of a larger system (i.e., station) and interacts with its neighbours by means of interfaces. Our first contribution comes in the form of a catalogue of elements that constitute the interfaces (as used in the Belgian railways) and associated contracts. Each interface can then be bound to a formal contract allowing its verification by the ocra tool. Our second contribution comes in the form of an algorithm designed to split the topology controlled by a single interlocking into components. The verification of a large station can therefore be achieved by verifying its constituting components and their interaction thereby tackling the state space explosion problem while providing guarantees on the whole interlocking.
Tags: ocra, nuXMV, railway, model-checking, compositional verification
- BibTeX Record
@INPROCEEDINGS{lvl-2018-962145, TITLE = {A Framework for the Formal Verification of Networks of Railway Interlockings - Application to the Belgian Railway}, AUTHOR = {Christophe Limbrée and Charles Pecheur}, YEAR = {2018}, URL = {https://lvl.info.ucl.ac.be/Publications/AFrameworkForTheFormalVerificationOfNetworksOfRailwayInterlockings-ApplicationToTheBelgianRailway}, }