View in EDS

Exploring the ERTMS/ETCS full moving block specification: an experience with formal methods.

Saved in:
Bibliographic Details
Title: Exploring the ERTMS/ETCS full moving block specification: an experience with formal methods.
Authors: Basile, Davide1 (AUTHOR) davide.basile@isti.cnr.it, ter Beek, Maurice H.1 (AUTHOR), Ferrari, Alessio1 (AUTHOR), Legay, Axel2 (AUTHOR)
Source: International Journal on Software Tools for Technology Transfer. Jun2022, Vol. 24 Issue 3, p351-370. 20p.
Subjects: Railroads, Joint ventures, Railroad trains, Statistical models
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 industry. [ABSTRACT FROM AUTHOR]
Copyright of International Journal on Software Tools for Technology Transfer is the property of Springer Nature and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Database: Engineering Source
Description
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 industry. [ABSTRACT FROM AUTHOR]
ISSN:14332779
DOI:10.1007/s10009-022-00653-3