Structural Abstraction and Selective Refinement for Formal Verification

要約

ロボットアプリケーションの安全検証は、ロボットが通常動作する環境の複雑さのために非常に困難です。モデルチェックによる正式な検証は保証を提供しますが、環境の複雑なモデルには長すぎるか失敗することさえあります。
通常のソリューションアプローチは、抽象化であり、より正確には行動的な抽象化です。
私たちの新しいアプローチでは、代わりに構造的抽象化を導入します。これは、ロボット環境のボクセル表現のコンテキストで調査しました。
この種の抽象化は、抽象的なボクセルにつながります。
また、ロボットアプリケーションの既存の方法論に基づいた完全で自動化された検証ワークフローを提案し、カウンターエクサムガイド付き抽象化洗練（CEGAR）の背後にある重要なアイデアに触発され、最初の抽象化を実行し、モデルの走行と絡み合ったカウンターエクサムに基づいて洗練を連続的に導入します。
したがって、私たちのアプローチは、構造抽象化の選択的改良を使用して、モデルチェックのランタイム効率を改善します。
私たちのアプローチの完全に自動化された実装は、数分でかなり高い（最大）解像度を備えた現実的なシナリオでカウンターエクササイズが見つかったため、その実行可能性を示しました。

要約(オリジナル)

Safety verification of robot applications is extremely challenging due to the complexity of the environment that a robot typically operates in. Formal verification with model-checking provides guarantees but it may often take too long or even fail for complex models of the environment. A usual solution approach is abstraction, more precisely behavioral abstraction. Our new approach introduces structural abstraction instead, which we investigated in the context of voxel representation of the robot environment. This kind of abstraction leads to abstract voxels. We also propose a complete and automated verification workflow, which is based on an already existing methodology for robot applications, and inspired by the key ideas behind counterexample-guided abstraction refinement (CEGAR) – performing an initial abstraction and successively introducing refinements based on counterexamples, intertwined with model-checker runs. Hence, our approach uses selective refinement of structural abstractions to improve the runtime efficiency of model-checking. A fully-automated implementation of our approach showed its feasibility, since counterexamples have been found for a realistic scenario with a fairly high (maximal) resolution in a few minutes, while direct model-checker runs led to a crash after a couple of days.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google