Validation and Real-Life Demonstration of ETCS Hybrid Level 3 Principles Using a Formal B Model


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 sub-sections 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 sub-sections 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 sub-section 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.

In Software Tools for Technology Transfer, Springer
Sebastian Krings
Sebastian Krings
Software Engineer

My interests include software analysis, formal methods and offensive security.