Formal methods in railway applications
Even in systems with low complexity, it is a challenge to ensure correct behaviour, interoperability, safety and reliability. This challenge is very real for modern rail control and signalling, such as the ERTMS interoperability standard. Schedules to deliver such systems are long and hardly predictable, and systems are costly to procure, develop and maintain. One of the main root causes for these problems is that tender requirements often tend to be vague and imprecise:
- Significant effort and know-how is needed to interpret and detail requirements, leading to critical design choices and interfaces whose impact is not understood until late phases.
- Design choices may lead to systems being based on proprietary solutions (“vendor lock-in”).
- Vague and imprecise requirements complicate the process to verify that systems comply with their requirements, and assessment of their safety.
- The need to implement changes is discovered late, when changes are expensive to perform.
Another main root cause, in part a consequence of vague and imprecise tender requirements, is that verification is mainly based on traditional methods such as review and test:
- These methods are time-consuming and error-prone, and verification coverage for critical system properties is poor; they can only detect issues, not prove absence.
- Traditional verification methods applied using imprecise requirements necessitates senior staff to manage such verification work, and to judge quality and safety.
- It becomes complex to grasp on what basis systems are assessed to be safe and in compliance with requirements, affecting system delivery schedules, maintenance and life-cycle costs.
Requirements on safety, security, and reliability in railway signalling are complex since they cover a vast state space, and because they use many concepts from multiple domains. To ensure that such requirements are satisfied is only possible by using Formal Methods in specification, development and verification. Formal methods provide techniques and tools to define and precisely analyse such concepts and relationships, and to verify requirements exhaustively. In addition to improved verification of critical system properties to reduce time-to-market and cost, formal methods can also improve requirement quality and reliability. Successful applications in the railway domain demonstrate these benefits, and that the number of defects becomes reduced.
A related topic that will be investigated within this mission is pertaining to the evaluation of artificial intelligence-based functions. The introduction of AI in some critical functions in railway command and control must, indeed, be undertaken while ensuring high safety levels.
The selected candidate will be in charge of and/or participate to the followings:
- - Development of semi-formal and formal models for some selected use case systems;
- - Application of formal methods on the use cases selected;
- - Specification and V&V for standard interfaces;
- - Safety analysis of AI-based functions (Artificial intelligence)
- - Participation in various coordination meetings (possible travels in France and abroad);
- - Participation to project meetings with all European partners;
- - Participation to the management of other possible involved persons (students, etc.).
- - Contribution to the achievement of deliverables and scientific publications.