Toward Usable Formal Models for Safety and Performance Evaluation of ERTMS/ETCS Level 3; The PERFORMINGRAIL Project

Within modern railways, Moving Block (MB) signalling systems represent the most efficient approach to ensure train separation. MB is a central concept in ERTMS/ETCS L3 (European Railway Traffic Management System / European Train Control System Level 3), which is an European standard for interoperable railways. Compared to traditional fixed block signalling, MB allows for substantial capacity gains at reduced costs, while improving availability as the trackside equipment would be substantially reduced. A set of specifications for MB operation has been proposed in the framework of previous research, but additional activities need to be undertaken to define detailed specifications for a safe and performable implementation of ETCS L3. In this respect, railway safety standards recommend the use of formal modelling and verification techniques to guarantee behavioural correctness and to validate safety requirements. However, there are several challenges to be tackled to make formal methods usable in industry, due to modelling difficulties and scalability to complex systems and scenarios. The work reported in this paper has been developed within the EU-funded project named PERFORMINGRAIL. We present a methodology showing how high-level MB specifications expressed in SysML can be transformed into reusable parametric formal models in order to enable automated verification and performance evaluation of MB systems. We apply the methodology to selected ETCS L3 scenarios for illustrative purposes.