Future-oriented research programme relies on railway expertise from Thales

 Photo Credit: AVL List GmbH

The findings from the research project make it possible to reduce resources, increase efficiency and sustainably improve safety in the field of verification and validation approaches for highly automated safe and secure systems.


Current verification and validation approaches for safety critical systems cause high efforts. Pure simulation is limited in modelling and computation and cannot cover physics in detail. Real-world tests consume too many resources and are potentially dangerous.

The European Initiative ENABLE-S3 aimed to substitute today’s cost-intensive verification & validation efforts by more advanced and efficient methods. From 2016 to 2019 the ENABLE-S3 team – consisting of 68 partners from 16 countries – put its research focus on establishing a comprehensive platform for the cost-effective validation and verification of autonomous and highly automated means of transport, satellites and medical examination equipment.

Thales participated in this large scale research project on novel verification and validation approaches for highly automated safe and secure systems. Thales was represented by experts from Austria.


ENABLE-S3 outcomes will facilitate the market introduction of automated systems in Europe and set the basis for future standards in this field.


Source: www.enable-s3.eu


Rail domain section relies on Thales lead

The main goal of a railway network operator is to provide a punctual and safe train service. Automation and computer driven train control are essential elements towards achieving such a service for large and complex railway systems. In ENABLE-S3, Thales coordinated a team of experts to develop a novel approach to verification and validation, with special focus on reducing the associated costs by the use of formal methods.


Railway specific knowledge combined with

More and more, formal methods for verification and validation are required in tenders worldwide. CENELEC, the European Committee for Electrotechnical Standardisation, highly recommends the use of formal methods.

But what is the benefit?

In current verification and validation approaches, test scenarios are carried out to demonstrate, that the design is correct and fulfills all requirements. Formal methods use mathematically based techniques to further proof the consistency, completeness and correctness of requirements assuming given semantics.  It is a highly reliable concept to detect possible problems in the earliest stages of system and software development to avoid higher adaption costs later in this process.


Fruitful cooperation with University of Southampton and Austrian Institute of Technology (AIT)

To put theory into practice, Thales developed the „Railground model“– the first model to verify and validate a signalling specification using formal methods. The model served as a basis for cooperation with universities and research institutes. Together with the University of Southampton Thales was able to mathematically validate the model while together with AIT test cases could be generated out of it.

Based on this experience, Thales could extend the Railground model to allow scenario based validation, which enables a domain specific engineer without mathematical background to make use of the formal methods.


Results applicable for several projects

ENABLE-S3 successfully presented the most important project results of three years of research at a public Final Event this May in Graz, Austria.

Picture: Enable-S3 Team - reailway section
Picture f.l.t.r.: Peter Tummeltshammer (Thales), Tomas Fischer (Thales), Gavin Crosmarie (APSYS), Colin Snook (Univ. of Southampton), Rupert Schlick (AIT)


Thales presented the findings in the rail domain section and where they have already been successfully implemented:

A new verification and validation (V&V) process including formal methods in the early stage of the process has been defined. Thales currently uses this formal method process successfully to verify ETCS (European Train Control System) Level 1 project data.


Within the research project, the formal method model has been used to verify and validate the “Hybrid ERTMS/ETCS Level 3” specification. The findings out of this mathematical method have been successfully included into the standardisation work. This validation has been used as a real-life case study during the ABZ 2018 conference in Southampton. The model together with several other works will be published as special edition of Springer's Software Tools for Technology Transfer in 2019.


A new redundancy architecture for the railway specific platform “TAS Platform” has been designed and verified using formal methods. It improved the efficiency of the design process by providing early feedback on the correctness of the algorithms. This architecture is already included in the current version of “TAS Platform”.


To sum up, using formal methods improves verification and validation efficiency and helps with detecting design flaws at an early stage of the development.


The output of this research project also led to several considerable publications, which are valuable readings for future research on this topic.