Shift2Rail is a joint undertaking funded by the EU via its Horizon 2020 program and by main railway stakeholders. Several Shift2Rail projects aim to investigate the application of formal methods to new ERTMS/ETCS railway signalling systems that promise to move European railway forward by guaranteeing high capacity, low cost and improved reliability. We explore the ERTMS/ETCS level 3 full moving block specifications stemming from different Shift2Rail projects using UPPAAL and statistical model checking. The results range from novel rigorously formalised requirements to an operational model formally verified against scenarios with multiple trains on a single railway line. From the gained experience, we have distilled future research goals to improve the formal specification and verification of real-time systems, and we discuss some barriers concerning a possible uptake of formal methods and tools in the railway industry
Exploring the ERTMS/ETCS full moving block specification: an experience with formal methods
Basile D;ter Beek MH;
2022
Abstract
Shift2Rail is a joint undertaking funded by the EU via its Horizon 2020 program and by main railway stakeholders. Several Shift2Rail projects aim to investigate the application of formal methods to new ERTMS/ETCS railway signalling systems that promise to move European railway forward by guaranteeing high capacity, low cost and improved reliability. We explore the ERTMS/ETCS level 3 full moving block specifications stemming from different Shift2Rail projects using UPPAAL and statistical model checking. The results range from novel rigorously formalised requirements to an operational model formally verified against scenarios with multiple trains on a single railway line. From the gained experience, we have distilled future research goals to improve the formal specification and verification of real-time systems, and we discuss some barriers concerning a possible uptake of formal methods and tools in the railway industryFile | Dimensione | Formato | |
---|---|---|---|
prod_466148-doc_183811.pdf
accesso aperto
Descrizione: Exploring the ERTMS/ETCS full moving block specification: an experience with formal methods
Tipologia:
Versione Editoriale (PDF)
Dimensione
2.34 MB
Formato
Adobe PDF
|
2.34 MB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.