Correct-by-Construction Design of Contextual Robotic Missions Using Contracts

要約

ロボットのミッションを効果的に指定して実装するには、ロボット システムのソフトウェア エンジニアリングに一連の課題が生じます。
これらの課題は、実際の運用環境におけるさまざまなアプリケーション シナリオや条件 (コンテキストとも呼ばれます) を考慮しながら、ロボットの高レベルのタスクを形式化して実行する必要があることから生じています。
複数のコンテキストを明示的に考慮した正しいミッション仕様を作成することは、面倒で間違いが発生しやすいものです。
さらに、コンテキストの数が増加し、その結果として仕様の複雑さが増すと、(合成手法を使用するなどにより) Correct-by-Construction 実装を生成することが困難になる可能性があります。
これらの問題に対処するための実行可能なアプローチは、ミッション仕様をより小さく管理しやすいサブミッションに分解し、各サブミッションを特定のコンテキストに合わせて調整することです。
それにもかかわらず、この構成的アプローチは、ミッション全体の正確性を確保する上で、独自の一連の課題をもたらします。
この論文では、保証保証契約を使用して状況に応じたロボットミッションを指定および実装するための新しい構成フレームワークを提案します。
ミッション仕様は階層的かつモジュール形式で構造化されており、各サブミッションを独立したロボット コントローラーとして合成できます。
事前に定義された条件下で正確性を確保しながら、サブミッション コントローラーを動的に切り替える問題に対処します。

要約(オリジナル)

Effectively specifying and implementing robotic missions poses a set of challenges to software engineering for robotic systems. These challenges stem from the need to formalize and execute a robot’s high-level tasks while considering various application scenarios and conditions, also known as contexts, in real-world operational environments. Writing correct mission specifications that explicitly account for multiple contexts can be tedious and error-prone. Furthermore, as the number of contexts, and consequently the complexity of the specification, increases, generating a correct-by-construction implementation (e.g., by using synthesis methods) can become intractable. A viable approach to address these issues is to decompose the mission specification into smaller, manageable sub-missions, with each sub-mission tailored to a specific context. Nevertheless, this compositional approach introduces its own set of challenges in ensuring the overall mission’s correctness. In this paper, we propose a novel compositional framework for specifying and implementing contextual robotic missions using assume-guarantee contracts. The mission specification is structured in a hierarchical and modular fashion, allowing for each sub-mission to be synthesized as an independent robot controller. We address the problem of dynamically switching between sub-mission controllers while ensuring correctness under predefined conditions.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google