Formal Methods for the Railway Sector

Researchers from the Formal Methods and Tools group of ISTI-CNR are working on a review and assessment of the main formal modelling and verification languages and tools used in the railway domain, with the aim of evaluating the actual applicability of the most promising ones to a moving block signalling system model.
The research is being conducted in the context of the EU H2020 Shift2Rail project ASTRail: SAtellite-based Signalling and Automation SysTems on Railways along with Formal Method and Moving Block Validation. The EU H2020 Shift2Rail initiative considers the use of formal methods to be fundamental to the provision of safe and reliable technological advances to increase the competitiveness of the railway industry, which include satellite-based train positioning (like, e.g., GNSS), train distancing based on moving block signalling systems and automatic driving.
Compared with other transport sectors, the railway sector is notoriously cautious about adopting technological innovations. This is due to the sector's robust safety requirements.
While GNSS-based positioning systems have been in use for quite some time now in the avionics and automotive sectors to provide accurate positioning and smart route planning, the current train separation systems are still based on fixed blocks. The length of the blocks, which depends on the safety margins established by the worst-case braking characteristics of trains and on the maximal allowed speed, determines the capacity of the line. With a moving block signalling system, in contrast, a safe zone around the moving train can be computed, thus optimising the line's exploitation (Figure 1). For this solution to work, it requires the precise absolute location, speed and direction of each train, to be determined by a combination of sensors and trainborne speedometers.
Hence, one of the current challenges in the railway sector consists of making moving block signalling systems as effective and precise as possible, while maintaining the high level of safety typical of railway transport; these new applications and solutions thus have to be carefully analysed, in terms of safety and performance, through the use of formal methods and tools during their development.
ASTRail will run until August 2019 and is coordinated by the Istituto Superiore Mario Boella sulle Tecnologie dell'Informazione e delle Telecomunicazioni (ISMB, Italy). Other partners are SIRTI S.p.A. (Italy), Ardanuy Ingeniería S.A. (Spain), École Nationale de l'Aviation Civile (ENAC, France), Union des Industries Ferroviaires Européennes (UNIFE, Belgium) and ISTI-CNR (Italy).