Towards Automatic Design and Verification for Level 3 of the European Train Control System
Robert Wille1,2,a, Tom Peham2,b, Judith Przigoda3,a and Nils Przigoda3,b
1Institute for Integrated Circuits, Johannes Kepler University Linz, Austria
2Software Competence Center Hagenberg GmbH (SCCH), Hagenberg, Austria
arobert.wille@jku.at
btom.peham@jku.at
3Siemens Mobility GmbH, Braunschweig, Germany
ajudith.przigoda@siemens.com
bnils.przigoda@siemens.com
ABSTRACT
For centuries, block signaling has been the fundamental principle of today’s railway systems to prevent trains from running into each other. But the corresponding infrastructure of physical blocks each requiring train detection methods is costly. Therefore, initiatives such as the European Train Control System (ETCS) and, here, particularly Level 3 of ETCS aim for the utilization of virtual sections which allow for a much higher degree of freedom and provide significant potential for increasing the efficiency in today’s train schedules. However, exploiting this potential is a highly non-trivial task which, thus far, mainly relied on manual labor. In this work, we provide an initial automatic methodology which aids designers of corresponding railway networks and train schedules. The methodology utilizes design automation expertise (here, in terms of satisfiability solvers) to unveil the potential of ETCS Level 3. Case studies (including a real-life example inspired by the Norwegian Railways) confirm the applicability and suitability of the proposed methodology.
