Cross–layer Formal Verification of Robotic Systems

要約

ロボット システムは、人間と対話したり、重要なタスクを実行したりするために広く使用されています。
そのため、彼らの行動について保証を提供することが不可欠です。
ロボット システムのモジュール性と複雑さのため、その設計と検証は多くの場合、いくつかの層に分割されます。
ただし、一部のシステム特性は、複数の層を同時に考慮することによってのみ調査できます。
具体的なロボットシステムの期待される特性を検証するためのクロスレイヤー検証手法を提案します。
私たちの方法では、他のレイヤーの抽象化を使用して 1 つのレイヤーを検証します。
我々は、抽象層のモデルを改良することと、検証中のプロパティを改良することの 2 つのアプローチを提案します。
これら 2 つのアプローチを組み合わせることは、モデルの汎用性を確保し、状態空間の爆発の問題を回避するために最も有望であると思われます。

要約(オリジナル)

Robotic systems are widely used to interact with humans or to perform critical tasks. As a result, it is imperative to provide guarantees about their behavior. Due to the modularity and complexity of robotic systems, their design and verification are often divided into several layers. However, some system properties can only be investigated by considering multiple layers simultaneously. We propose a cross-layer verification method to verify the expected properties of concrete robotic systems. Our method verifies one layer using abstractions of other layers. We propose two approaches: refining the models of the abstract layers and refining the property under verification. A combination of these two approaches seems to be the most promising to ensure model genericity and to avoid the state-space explosion problem.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google