Towards Automatic Design and Verification for Level 3 of the European Train Control System

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.