Formal Verification of Safety Architectures for Automated Driving

要約

安全アーキテクチャは、自動運転車 (ADV) の安全性を確保する上で重要な役割を果たします。
これらは、ブラックボックス ADV コントローラーの安全エンベロープとして、および 1 つの ODD から別の ODD への正常な劣化のために使用できます。
責任に敏感な安全性 (RSS) の形式化に関する以前の研究に基づいて、保証仮定推論とフォールバックのような構造に対応する新しいプログラム ロジックを導入します。
これにより、既存および新規の安全アーキテクチャの安全性を正式に定義し、証明することができます。
このロジックをプルオーバーシナリオに適用し、その結果得られる安全アーキテクチャを実験的に評価します。

要約(オリジナル)

Safety architectures play a crucial role in the safety assurance of automated driving vehicles (ADVs). They can be used as safety envelopes of black-box ADV controllers, and for graceful degradation from one ODD to another. Building on our previous work on the formalization of responsibility-sensitive safety (RSS), we introduce a novel program logic that accommodates assume-guarantee reasoning and fallback-like constructs. This allows us to formally define and prove the safety of existing and novel safety architectures. We apply the logic to a pull over scenario and experimentally evaluate the resulting safety architecture.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google