Publications

Verification of railway interlocking - Compositional approach with OCRA

Authors
Christophe Limbrée, Quentin Cappart, Charles Pecheur, Stefano Tonetta?
Tags
, , , ,
Title
Verification of railway interlocking - Compositional approach with OCRA
Authors
Christophe Limbrée, Quentin Cappart, Charles Pecheur, Stefano Tonetta?
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
Book title
Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification
Series
Lecture Notes in Computer Science
Volume
9707
Pages
134--149
Publisher
Springer International Publishing
Year
2016

Abstract

In the railway domain, an electronic interlocking is a com- puterised system that controls the railway signalling components (e.g. switches or signals) in order to allow a safe operation of the train traffic. Interlockings are controlled by a software logic that relies on a generic software and a set of application data particular to the station under control. The verification of the application data is time consuming and error prone as it is mostly performed by human testers. In the first stage of our research [3], we built a model of a small Belgian railway station and we performed the verification of the application data with the nusmv model checker. However, the verification of larger sta- tions fails due to the state space explosion problem. The intuition is that large stations can be split into smaller components that can be verified separately. This concept is known as compositional verification. This ar- ticle explains how we used the ocra tool in order to model a medium size station and how we verified safety properties by mean of contracts. We also took advantage of new algorithms (k-liveness and ic3) recently implemented in nuxmv in order to verify LTL properties on our model.

Tags Tags: , , , ,

BibTeX Record
  @INPROCEEDINGS{lvl-2016-452384,
    TITLE = {Verification of railway interlocking - Compositional approach with OCRA},
    AUTHOR = {Christophe Limbree and Quentin Cappart and Charles Pecheur and Stefano Tonetta},
    YEAR = {2016},
    VOLUME = {9707},
    PAGES =  {134--149},
    PUBLISHER = {Springer International Publishing},
    SERIES = {Lecture Notes in Computer Science},
    URL = {https://lvl.info.ucl.ac.be/Publications/VerificationOfRailwayInterlocking-CompositionalApproachWithOCRA},
  }