用形式化方法与安全盾牌验证AI列车系统的安全性
Using Formal Models, Safety Shields and Certified Control to Validate AI-Based Train Systems
- 用B方法对列车转向系统进行形式化分析确保安全
- 运行时证书检查器提升感知系统的可靠性
- 可在仿真中实时监控并验证安全属性，适合铁路AI验证
自动驾驶系统的认证是科学与工业中的重要课题。KI-LOK项目探索将AI组件安全集成到自动驾驶列车的新方法。采用双层策略：(1) 使用B方法进行形式化分析，保障转向系统安全；(2) 通过运行时证书检查器提升感知系统的可靠性。本文将两种方法整合进一个演示系统，该系统在正式模型上运行仿真，由真实AI输出和证书检查器控制，并集成至验证工具ProB。该系统支持运行时监控、运行时验证及基于形式化B模型的统计验证，可检测并分析AI与证书检查器的潜在漏洞。研究以信号检测为例，展示应用效果。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。