Title
Validation and real-life demonstration of ETCS hybrid level 3 principles using a formal B model
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 introduces virtual subsections as sub-divisions of classical track sections with trackside train detection. 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 virtual subsections using the train position reports, train integrity information, and the track occupation states. From the perspective of the RBC, the VBF behaves as an interlocking that transmits all signal aspects for virtual signals introduced for each virtual subsection 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.
Year
DOI
Venue
2020
10.1007/s10009-020-00551-6
International Journal on Software Tools for Technology Transfer
Keywords
DocType
Volume
B-method, Animation, Model-based testing, Model checking, ETCS
Journal
22
Issue
ISSN
Citations 
3
1433-2779
2
PageRank 
References 
Authors
0.38
0
8
Name
Order
Citations
PageRank
Dominik Hansen1263.23
Michael Leuschel22156135.89
Philipp Körner341.75
Sebastian Krings4258.93
Thomas Naulin520.38
Nader Nayeri620.38
David Schneider771.84
Frank Skowron820.38