Publications

A Framework for the Formal Verification of Networks of Railway Interlockings - Application to the Belgian Railway

Authors
Christophe Limbrée, Charles Pecheur
Tags
, , , ,
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 Tags: , , , ,

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},
  }