Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

Verification of interlocking systems using statistical model checking

Quentin Cappart 1 Christophe Limbrée 1 Pierre Schaus 1 Jean Quilbeuf 2, 3 Louis-Marie Traonouez 3 Axel Legay 3
2 ArchWare
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires
3 TAMIS - Threat Analysis and Mitigation for Information Security
IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL, Inria Rennes – Bretagne Atlantique
Abstract : In the railway domain, an interlocking is the system ensuring safe train traffic inside a station by controlling its active elements such as the signals or points. Modern interlockings are configured using particular data, called application data, reflecting the track layout and defining the actions that the interlocking can take. The safety of the train traffic relies thereby on application data correctness, errors inside them can cause safety issues such as derailments or collisions. Given the high level of safety required by such a system, its verification is a critical concern. In addition to the safety, an interlocking must also ensure that availability properties, stating that no train would be stopped forever in a station, are satisfied. Most of the research dealing with this verification relies on model checking. However, due to the state space explosion problem, this approach does not scale for large stations. More recently, a discrete event simulation approach limiting the verification to a set of likely scenarios, was proposed. The simulation enables the verification of larger stations, but with no proof that all the interesting scenarios are covered by the simulation. In this paper, we apply an intermediate statistical model checking approach, offering both the advantages of model checking and simulation. Even if exhaustiveness is not obtained, statistical model checking evaluates with a parametrizable confidence the reliability and the availability of the entire system.
Document type :
Preprints, Working Papers, ...
Complete list of metadata

Cited literature [19 references]  Display  Hide  Download
Contributor : Louis-Marie Traonouez Connect in order to contact the contributor
Submitted on : Thursday, November 17, 2016 - 3:46:36 PM
Last modification on : Wednesday, November 3, 2021 - 6:05:25 AM

Links full text


  • HAL Id : hal-01398649, version 1
  • ARXIV : 1605.02529


Quentin Cappart, Christophe Limbrée, Pierre Schaus, Jean Quilbeuf, Louis-Marie Traonouez, et al.. Verification of interlocking systems using statistical model checking. 2016. ⟨hal-01398649⟩



Les métriques sont temporairement indisponibles