Bosch Research Blog | 投稿者: Christian Heinzemann および Michaela Klauck、2024-05-13
このストーリーはボッシュリサーチブログの一部です
自動運転機能は、複雑な交通状況で正しい判断を下す必要があります。Bosch Research は、数学に基づく技術を使用して、あらゆる運転シナリオでこれらの判断が常に安全であることを証明しています。
自動運転車の運転能力を信頼していますか? 高速道路を運転していて、前方に遅い車が近づいてきたときを想像してください。車線を変更して追い越したいのですが、後ろからもっと速い車が来ています。車線変更しても安全でしょうか? これらは、運転中によく答えなければならない質問です。自動運転機能に頼る場合、ソフトウェアはあらゆる交通状況でこれらの質問に正しく答えることができなければなりません。現在、メーカーはどのようにして事故を可能な限り回避しているかをご存知ですか?
現在、信頼性は、実際の走行またはシミュレーションで何千キロものテスト走行を通じて得られます。テスト走行では、車はあらゆる運転シナリオにさらされます。当社では、数学的計算に基づく別の厳密なソリューションを提案します。これにより、開発プロセスのかなり早い段階で、指定された道路設定で考えられるすべての運転シナリオを完全にチェックできます。これにより、テストよりもはるかに低いコストと大幅に少ない労力で、車のソフトウェア（の一部）を検証できます。同時に、100% の信頼性とコーナーケースのカバレッジが保証されます。
自動運転アライアンスでは、ボッシュのクロスドメイン コンピューティング ソリューション (XC) 部門と CARIAD が協力して、市街地や高速道路での運転向けのレベル 2 ハンズフリー システムから、高速道路で車両を完全に制御するレベル 3 システムまで、自動運転機能を開発しています。人間のドライバーは、ハンドルから手を離すと、少なくとも部分的には制御不能になるため、これらの自動運転機能の安全性は非常に重要です。このような機能の中核となる要素の 1 つは、周囲の交通状況に基づいて、実行すべき高レベルのアクションを決定する動作プランナーです。動作プランナーによる決定は、あらゆる交通状況において安全であり、交通規則に準拠していることが重要です。
ボッシュとブルーノ・ケスラー財団との共同研究活動において、私たちは、テストよりもさらに優れた方法で、開発プロセスの早い段階でより高い精度でエラーを見つけることができるかどうか自問しました。
私たちのアイデアは、コンピュータ サイエンスの形式手法を使用して、ソフトウェア (の一部) が安全要件を満たしていることを実際に証明することでした。特に、完全に自動化できるモデル チェックと呼ばれる手法を調査しました。モデル チェックの利点の 1 つは、システムが要件を満たしていないシステム実行を特定できることです。反例と呼ばれるこれらの実行は、開発者が視覚化して検査し、それに応じてソフトウェアに変更や改善を加えることができます。
私たちの目標は、モデル チェッキングをエンジニアの開発プロセスに可能な限りシームレスに統合することでした。これは、私たちが開発したツールチェーンの 2 つの主要な部分によって実現されました。まず、開発者は、現在のバージョンのビヘイビア プランナーでモデル チェッカーを使用するのに最小限の労力しかかかりません。必要なモデルは、プランナーが指定されている C++ コードから自動的に抽出され、コードに必要なのはいくつかの注釈だけです。Bosch Research として、私たちは主に検証手順用の環境モデルを開発し、提供しました。このモデルは、道路環境と交通状況における他の車の動作を表します。検証には、Fondazione Bruno Kessler によって開発された nuXmv モデル チェッカーを使用しました。モデリング手順の小さな変更でもパフォーマンスに大きな影響を与える可能性があるため、効率的なモデル チェックのためのモデルの作成と設計に関する彼らの専門知識は不可欠でした。
第二に、モデルチェッカーによって提供される反例は、開発者がフィードバック ループで直接使用して動作プランナーに変更や改善を加えることができるため、モデルチェッカーによって検出された仕様違反が将来のバージョンで排除されることが保証されます。反例は、視覚化の自動生成によって開発者が簡単に理解および解釈できるようになります。動作プランナーのモデルを C++ コードから自動的に抽出し、nuXmv モデルチェッカーを統合し、チェックされた仕様に違反する動作の視覚化を自動生成することで、自動運転で使用される動作プランナー用の効率的でユーザー フレンドリな検証ツールチェーンを開発できました。このツールチェーンは開発プロセスに簡単に統合でき、モデル チェックの知識がなくても自動運転エンジニアが使用できます。
私たちの論文「安全な自動運転に向けて：開発中の行動プランナーのモデル検証」が「ETAPS 2024」で「TACAS Distinguished Artifact Award」を受賞し、私たちの研究の重要性がさらに強調されたことをお知らせいたします。
この成果は、Bosch Research、Fondazione Bruno Kessler、CARIAD の共同作業の証です。私たちは、優れた成果物とその使用方法に関する明確な説明を提供したことが認められただけでなく、業界紙の一部として一般に公開された成果物を公開できたことを非常に誇りに思っています。
さらに興味が湧いたら、Zenodo の受賞歴のあるコード アーティファクトをご覧ください。仕様に違反する動作プランナーから始めて、モデル チェックを行い、安全性を確保するための変更を加えるという完全な手順を自分で試すことができます。
ぜひご共有いただくか、直接お問い合わせください。
Christian は、Bosch Corporate Research の「高度なデジタルおよび AI ソリューション」部門の「信頼できるサイバーフィジカル ソフトウェア エンジニアリング」クラスターに所属する自律システム検証の上級専門家です。2015 年に Bosch に入社し、自律ロボットの検証に携わっています。現在 Christian は、安全な計画機能の開発と、自動運転機能の計画および意思決定の検証に関する研究活動を主導しています。彼の研究の主な焦点は、形式手法と検証を産業実践に取り入れることです。以前は、Paderborn 大学および Fraunhofer Institute for Mechatronic Systems Design (IEM) で研究員として働いていました。Paderborn 大学でコンピューター サイエンスの博士号を取得しています。
ミカエラは、ボッシュ コーポレート リサーチの「高度なデジタルおよび AI ソリューション」部門の「ディペンダブル サイバーフィジカル ソフトウェア エンジニアリング」クラスターの研究エンジニアです。彼女の専門は、自律システムにおける計画と意思決定の検証です。2023 年から、ボッシュでロボットの検討と自律運転動作のモデル チェックに取り組んでいます。現在は、EU 資金提供プロジェクトを含むロボティクス ポートフォリオの CONVINCE アクティビティを主導しており、モデル チェック技術を使用して自律ロボットの動作をより堅牢にすることに取り組んでいます。以前は、ザールラント大学の研究員として、定量的検証の分野、特にこれらのトピックと自動計画および AI コミュニティとのインターフェイスに取り組んでいました。彼女はコンピューター サイエンスの博士号を取得しています。論文: 「システム検証のための確率的モデル チェック、計画、学習のつながりについて」。
元記事: https://www.bosch.com/stories/safe-automated-driving/