Toward Usable Formal Models for Safety and Performance Evaluation of ERTMS/ETCS Level 3: The PERFORMINGRAIL Project
| Autor: | Saddem-yagoubi, Rim, Sanwal, Muhammad Usman, Libutti, Simone, Benerecetti, Massimo, Beugin, Julie, Flammini, Francesco, Ghazel, Mohamed, Janssen, Bob, Marrone, Stefano, Mogavero, Fabio, Nardone, Roberto, Peron, Adriano, Seceleanu, Cristina, Vittorini, Valeria |
|---|---|
| Přispěvatelé: | Évaluation des Systèmes de Transports Automatisés et de leur Sécurité (COSYS-ESTAS ), Université Gustave Eiffel, Mälardalen University College, Mälardalen University (MDH), Department of Electrical Engineering and Information Technologies, University of Naples Federico II, Eulynx, Department of Mathematics and Physics, University of Campania, Department of Engineering, University of Naples Parthenope, PERFORMINGRAIL |
| Jazyk: | angličtina |
| Rok vydání: | 2022 |
| Předmět: | |
| Zdroj: | ESREL 2022, 32nd European Safety and Reliability Conference ESREL 2022, 32nd European Safety and Reliability Conference, Aug 2022, Dublin, France. 8p |
| Popis: | ESREL 2022, 32nd European Safety and Reliability Conference, Dublin, IRELANDE, 28-/08/2022 - 01/09/2022; 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|