Exploring the ERTMS/ETCS full moving block specification: an experience with formal methods
Basile D., Ter Beek M. H., Ferrari A., Legay A.
Formal methods Railways ERTMS/ETCS Moving block UPPAAL Statistical model checking
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
Source: International journal on software tools for technology transfer (Internet) 24 (2022): 351–370. doi:10.1007/s10009-022-00653-3
Publisher: Springer, Berlin , Germania
Metrics
Back to previous page
@article{oai:it.cnr:prodotti:466148,
title = {Exploring the ERTMS/ETCS full moving block specification: an experience with formal methods},
author = {Basile D. and Ter Beek M. H. and Ferrari A. and Legay A.},
publisher = {Springer, Berlin , Germania},
doi = {10.1007/s10009-022-00653-3},
journal = {International journal on software tools for technology transfer (Internet)},
volume = {24},
pages = {351–370},
year = {2022}
}
0000-0002-7196-6609ISTI Repository
DOIAlso available from
