An Event-B Model of the Hybrid ERTMS/ETCS Level 3 Standard

Amel Mammar, Marc Frappier, Steve Jeffrey Tueno Fotso, Régine Laleau
Case Study Digital Printed Abstract View Cite Source
Type
Conference paper
Publication
6th International Conference on ASM, Alloy, B, TLA, VDM, and Z (ABZ'18)

Abstract

This paper presents an Event-B model of the ABZ2018 case study on the European Rail Traffic Management System (ERTMS) standard. The case study focusses on the management of fixed virtual sub-sections (VSS). We model the hybrid level 3 of the standard, which assumes that trains may be either equipped with an on-board train integrity monitoring system (TIMS) and that they report their position and integrity, ERTMS trains not fitted with TIMS that report only their front position or non-ERTMS trains that do not report any information about their position. We take into account most of the main features of the case study. Our model is decomposed into four refinements. All proof obligations have been discharged using the Rodin provers, except those related to the computation of the VSS state machine, which was found to be ambiguous (nondeterministic). Our model has been validated using ProB. The main safety property, which is that ERTMS trains do not collide, is proved.

Document

Reference

% BibTex
@inproceedings{DBLP:conf/asm/MammarFFL18,
  author    = {Amel Mammar and
               Marc Frappier and
               Steve Jeffrey Tueno Fotso and
               R{\'{e}}gine Laleau},
  title     = {An Event-B Model of the Hybrid {ERTMS/ETCS} Level 3 Standard},
  booktitle = {Abstract State Machines, Alloy, B, TLA, VDM, and {Z} - 6th International
               Conference, {ABZ} 2018, Southampton, UK, June 5-8, 2018, Proceedings},
  pages     = {353--366},
  year      = {2018},
  crossref  = {DBLP:conf/asm/2018}
	}

Sources

For more information, please contact the authors

ABZ'18

Related