Using Formal Models, Safety Shields and Certified Control to Validate AI-Based Train Systems
Not on the map. Why?
Abstract (arXiv)
The certification of autonomous systems is an important concern in science and industry. The KI-LOK project explores new methods for certifying and safely integrating AI components into autonomous trains. We pursued a two-layered approach: (1) ensuring the safety of the steering system by formal analysis using the B method, and (2) improving the reliability of the perception system with a runtime certificate checker. This work links both strategies within a demonstrator that runs simulations on the formal model, controlled by the real AI output and the real certificate checker. The demonstrator is integrated into the validation tool ProB. This enables runtime monitoring, runtime verification, and statistical validation of formal safety properties using a formal B model. Consequently, one can detect and analyse potential vulnerabilities and weaknesses of the AI and the certificate checker. We apply these techniques to a signal detection case study and present our findings.
Key facts. No citing papers in the map yet (data through 14 Oct 2026). Builds on 12 of its 37 references that are in the map. First posted on arXiv 21 Nov 2024.
Builds on
12 of 37 references.
References · 12
- 2015You Only Look Once: Unified, Real-Time Object Detectioncited by 4,852
- 2019Scalability in Perception for Autonomous Driving: Waymo Open Datasetcited by 2,451
- 2017CARLA: An Open Urban Driving Simulatorcited by 2,449
- 2017Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networkscited by 744
- 2016Safety Verification of Deep Neural Networkscited by 263
- 2018Reachability Analysis of Deep Neural Networks with Provable Guaranteescited by 93
- 2020The Probabilistic Model Checker Stormcited by 66
- 2023Closed-loop Analysis of Vision-based Autonomous Systems: A Case Studycited by 18
- 2021Systematic Literature Review of Validation Methods for AI Systemscited by 10
- 2023TrainSim: A Railway Simulation Framework for LiDAR and Camera Dataset Generationcited by 7
- 2021Certified Control: An Architecture for Verifiable Safety of Autonomous Vehiclescited by 5
- 2023Certified Control for Train Sign Classificationcited by 1
Built on by
Not cited yet.