Using Formal Models, Safety Shields and Certified Control to Validate AI-Based Train Systems
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866915029949874176 |
|---|---|
| author | Gruteser, Jan Roßbach, Jan Vu, Fabian Leuschel, Michael |
| author_facet | Gruteser, Jan Roßbach, Jan Vu, Fabian Leuschel, Michael |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2411_14374 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Using Formal Models, Safety Shields and Certified Control to Validate AI-Based Train Systems Gruteser, Jan Roßbach, Jan Vu, Fabian Leuschel, Michael Logic in Computer Science Artificial Intelligence Computer Vision and Pattern Recognition 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. |
| title | Using Formal Models, Safety Shields and Certified Control to Validate AI-Based Train Systems |
| topic | Logic in Computer Science Artificial Intelligence Computer Vision and Pattern Recognition |
| url | https://arxiv.org/abs/2411.14374 |