A Formal Methods Demonstrator for Railways

The 4SECURail project - funded by the European Union Horizon 2020 Shift2Rail Joint Undertaking - has two overall objectives: to design a Computer Security Incident Response Team (CSIRT) for joint EU-Rail cybersecurity, and the setup of a Formal Methods Demonstrator for the evaluation, in terms of cost, benefits and required learning curve, of the impact of the use of Formal Methods for the rigorous specification of the components of a railway signalling infrastructure.

While it is recognized that the adoption by the railways infrastructure managers of a rigorous specification methodology based on formal methods would definitely improve the dependability of the subsystems - that still have to guarantee the safety and availability of the overall infrastructure even when they are likely to be developed by the different suppliers - a detailed analysis of the costs, benefits, and of the required learning curve, of such adoption of formal methods is still missing.

As part of the first Work Stream of the project, researchers from the Formal Methods and Tools group of ISTI-CNR will shed more light on this issue with the design of a Formal Methods Demonstrator to evaluate the potential impact of the use of Formal Methods within a system specification process that could be adopted by railway infrastructure managers. The ISTI-CNR demonstrator design efforts will be complemented in the project by SIRTI for the selection and specification of signaling subsystem to be used as case study, and by FIT Consulting for development of the Cost/Benefits analysis.

The second Work Stream of the project, led by Hit Rail B.V. with the collaboration of UIC (International Union of Railways) and Tree Technology, will deliver a collaboration platform for a European Railway Computer Security Incident Response Team (CSIRT), designed to coordinate the Cyber Security response actions of the separate railway security teams.

The 4SECURail project which has started in December 1st 2019 and it is expected to end in November 30th 2021, is coordinated by engineering consulting firm Ardanuy Ingeniería, S.A.


Please contact:
Franco Mazzanti
Coordinator of the Work Stream 1 on Formal Methods