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.
Type de document :
Pré-publication, Document de travail
2016
Liste complète des métadonnées

Littérature citée [19 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01398649
Contributeur : Louis-Marie Traonouez <>
Soumis le : jeudi 17 novembre 2016 - 15:46:36
Dernière modification le : vendredi 16 novembre 2018 - 01:23:06

Lien texte intégral

Identifiants

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

Citation

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〉

Partager

Métriques

Consultations de la notice

538