Formal verification for the safety of railway moving block operations – 4RaiMBO

Formal methods are mathematical techniques that allow for describing and verifying properties in hardware and software systems [1]. They provide a rigorous framework for specifying, developing, and ensuring the quality and safety of critical systems. Formal methods are used in several domains. In the context of railway systems, the transport mode with the lowest CO2 emissions, demand for passenger transport is expected to increase by 40% by 2050. To meet this demand, building new railway lines is very expensive and sometimes not feasible due to urban constraints and lack of space. An alternative solution is to implement the next generation of signalling systems, based on the concept of Moving Block (MB) system, and capable of optimising the management of train traffic. The principle of MB is to separate trains using an absolute braking distance (the distance required to reach a stopping point) coupled with a safety margin. As a result, it promises significant benefits in terms of line capacity, installation and operation costs, reliability and interoperability [2]. However, the full specifications for MB system are still under development and will require further refinement before it can be considered as a viable and, above all, safe solution for European railways. In the context of this project, we will contribute to the verification and the validation of MB system specifications. The idea is to generate an ontology for MB system from the system specifications and to propose a modelling approach for the development of formal models using the defined ontology.
The primary objectives of the project are:
Objective 1: Define an ontology for MB system based on the analysis of system specifications.
Objective 2: Develop a methodology for generating formal models from the defined ontology.
Objective 3: Represent some operational scenarios using formal modelling and investigate safety and functional features by means of formal methods and/or simulation.