Using Formal Models, Safety Shields and Certified Control to Validate AI-Based Train Systems

要約

自律システムの認証は、科学と産業において重要な関心事です。
KI-LOK プロジェクトでは、AI コンポーネントを認証し、自動運転列車に安全に統合するための新しい方法を模索しています。
（1）B法による形式解析によるステアリングシステムの安全性の確保、（2）ランタイム証明書チェッカーによる知覚システムの信頼性向上の2層のアプローチを追求しました。
この作業では、実際の AI 出力と実際の証明書チェッカーによって制御される、正式なモデル上でシミュレーションを実行するデモンストレーター内で両方の戦略をリンクします。
デモンストレーターは検証ツール ProB に統合されています。
これにより、フォーマル B モデルを使用したランタイム監視、ランタイム検証、およびフォーマル安全特性の統計的検証が可能になります。
その結果、AI と証明書チェッカーの潜在的な脆弱性と弱点を検出して分析できます。
これらの技術を信号検出のケーススタディに適用し、その結果を紹介します。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google