Using a Formal B Model at Runtime in a Demonstration of the ETCS Hybrid Level 3 Concept with Real Trains

Dominik Hansen, Michael Leuschel, David Schneider, Sebastian Krings, Philipp Körner, Thomas Naulin, Nader Nayeri, Frank Skowron
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

In this article, we present a concrete realisation of the ETCS Hybrid Level 3 concept, whose practical viability was evaluated in a field demonstration in 2017. Hybrid Level 3 (HL3) introduces Virtual SubSections (VSS) as sub-divisions of classical track sections with Trackside Train Detection (TTD). Our approach introduces an add-on for the Radio Block Centre (RBC) of Thales, called Virtual Block Function (VBF), which computes the occupation states of the VSSs according to the HL3 concept using the train position reports, train integrity information, and the TTD occupation states. From the perspective of the RBC, the VBF behaves as an Interlocking (IXL) that transmits all signal aspects for virtual signals introduced for each VSS to the RBC. We report on the development of the VBF, implemented as a formal B model executed at runtime using ProB and successfully used in a field demonstration to control real trains.

Document

Reference

% BibTex
@inproceedings{hansen2018using,
  title={Using a formal B model at runtime in a demonstration of the ETCS hybrid level 3 concept with real trains},
  author={Hansen, Dominik and Leuschel, Michael and Schneider, David and Krings, Sebastian and K{\"o}rner, Philipp and Naulin, Thomas and Nayeri, Nader and Skowron, Frank},
  booktitle={International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z},
  pages={292--306},
  year={2018},
  organization={Springer}
}

Sources

  • Used formal method: Classical B

  • Resources and tools: ProB

    For more information, please contact the authors

ABZ'18

Related