Future-oriented research programme relies on railway expertise from Thales
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.
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.
Thales presented the findings in the rail domain section and where they have already been successfully implemented:
The output of this research project also led to several considerable publications, which are valuable readings for future research on this topic.