Publications

Verification of railway interlocking systems

Authors
Simon Busard, Quentin Cappart, Christophe Limbrée, Charles Pecheur, Pierre Schaus
Tags
, ,
Title
Verification of railway interlocking systems
Authors
Simon Busard, Quentin Cappart, Christophe Limbrée, Charles Pecheur, Pierre Schaus
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
Proceedings 4th International Workshop on Engineering Safety and Security Systems, Oslo, Norway, June 22, 2015
Series
Electronic Proceedings in Theoretical Computer Science
Volume
184
Pages
19-31
Publisher
Open Publishing Association
Editor
ang, Jun and Liu, Yang and Mauw, Sjouke
Year
2015

Abstract

In the railway domain, an interlocking is a computerised system that controls the railway signalling objects in order to allow a safe operation of the train traffic. Each interlocking makes use of particular data, called application data, that reflects the track layout of the station under control. The verification and validation of the application data are performed manually and is thus error-prone and costly. In this paper, we explain how we built an executable model in NuSMV of a railway interlocking based on the application data. We also detail the tool that we have developed in order to translate the application data into our model automatically. Finally we show how we could verify a realistic set of safety properties on a real-size station model by customizing the existing model-checking algorithm with PyNuSMV a Python library based on NuSMV.

Tags Tags: , ,

BibTeX Record
  @INPROCEEDINGS{lvl-2015-225165,
    TITLE = {Verification of railway interlocking systems},
    AUTHOR = {Simon Busard and Quentin Cappart and Christophe Limbr\ee and },
    YEAR = {2015},
    VOLUME = {184},
    PAGES =  {19-31},
    PUBLISHER = {Open Publishing Association},
    EDITOR = {ang and Jun and Liu and Yang and Mauw and Sjouke},
    SERIES = {Electronic Proceedings in Theoretical Computer Science},
    URL = {https://lvl.info.ucl.ac.be/Publications/VerificationOfRailwayInterlockingSystems},
  }