論文の概要: A Compositional Approach to Verifying Modular Robotic Systems
- arxiv url: http://arxiv.org/abs/2208.05507v2
- Date: Thu, 30 Nov 2023 17:02:05 GMT
- ステータス: 処理完了
- システム内更新日: 2023-12-01 20:54:38.631953
- Title: A Compositional Approach to Verifying Modular Robotic Systems
- Title(参考訳): モジュール型ロボットシステムに対する構成的アプローチ
- Authors: Matt Luckcuck and Marie Farrell and Angelo Ferrando and Rafael C.
Cardoso and Louise A. Dennis and Michael Fisher
- Abstract要約: 本稿では,ロボットオペレーティング・システム(ROS)を用いたロボットシステムにおけるノードの特定のための構成的アプローチについて述べる。
我々は,これらのノードレベルの契約の構成を容易にする推論ルールを導入し,システムレベルの特性を導出する。
また、ノードのFOL仕様をキャプチャし、この契約を実装にリンクする新しいDomain-Specific Language、ROS Contract Languageも提示します。
- 参考スコア(独自算出の注目度): 1.385411134620987
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Robotic systems used in safety-critical industrial situations often rely on
modular software architectures, and increasingly include autonomous components.
Verifying that these modular robotic systems behave as expected requires
approaches that can cope with, and preferably take advantage of, this inherent
modularity. This paper describes a compositional approach to specifying the
nodes in robotic systems built using the Robotic Operating System (ROS), where
each node is specified using First-Order Logic (FOL) assume-guarantee contracts
that link the specification to the ROS implementation. We introduce inference
rules that facilitate the composition of these node-level contracts to derive
system-level properties. We also present a novel Domain-Specific Language, the
ROS Contract Language, which captures a node's FOL specification and links this
contract to its implementation. RCL contracts can be automatically translated,
by our tool Vanda, into executable monitors; which we use to verify the
contracts at runtime. We illustrate our approach through the specification and
verification of an autonomous rover engaged in the remote inspection of a
nuclear site, and finish with smaller examples that illustrate other useful
features of our framework.
- Abstract(参考訳): 安全クリティカルな産業状況で使用されるロボットシステムは、しばしばモジュラーソフトウェアアーキテクチャに依存し、ますます自律的なコンポーネントを含んでいる。
これらのモジュラーロボットシステムが期待通りに振る舞うことを検証するには、この固有のモジュラリティに対処し、好ましくは活用できるアプローチが必要である。
本稿では,ロボットオペレーティングシステム (ros) を用いて構築されたロボットシステムにおいて,各ノードを1次論理 (fol) の前提言語契約で指定し,その仕様をros実装にリンクする構成的手法について述べる。
我々は,これらのノードレベルの契約の構成を容易にする推論ルールを導入し,システムレベルの特性を導出する。
また、ノードのFOL仕様をキャプチャし、この契約を実装にリンクする新しいDomain-Specific Language、ROS Contract Languageも提示します。
RCL契約は、当社のツールであるVandaによって、実行可能モニタに自動的に変換できます。
我々は,核施設の遠隔検査に携わる自律ローバーの仕様と検証を通じて,我々のアプローチを説明し,我々のフレームワークの他の有用な特徴を示す小さな例で仕上げる。
関連論文リスト
- A General Verification Framework for Dynamical and Control Models via
Certificate Synthesis [60.03938402120854]
システム仕様を符号化し、対応する証明書を定義するためのフレームワークを提供する。
コントローラと証明書を形式的に合成する自動化手法を提案する。
我々のアプローチは、ニューラルネットワークの柔軟性を利用して、制御のための安全な学習の幅広い分野に寄与する。
論文 参考訳(メタデータ) (2023-09-12T09:37:26Z) - Correct-by-Construction Design of Contextual Robotic Missions Using
Contracts [6.890369837091434]
本稿では,コンテキストロボットのミッションを規定し,実装するための新しい構成フレームワークを提案する。
ミッション仕様は階層的でモジュラーな方法で構成されており、各サブミッションを独立したロボットコントローラとして合成することができる。
論文 参考訳(メタデータ) (2023-06-13T21:29:17Z) - Monitoring ROS2: from Requirements to Autonomous Robots [58.720142291102135]
本稿では,構造化自然言語で記述された要件から自律ロボットのランタイムモニタを生成するための形式的アプローチの概要について述べる。
当社のアプローチでは,Fletal Requirement Elicitation Tool (FRET) とランタイム検証フレームワークであるCopilotを,Ogma統合ツールを通じて統合しています。
論文 参考訳(メタデータ) (2022-09-28T12:19:13Z) - Composing Complex and Hybrid AI Solutions [52.00820391621739]
一般的なAIアプリケーションで上記の機能を実現するためのAcumosシステムの拡張について述べる。
当社の拡張機能には、gRPC/Protobufインターフェースによるより汎用的なコンポーネントのサポートが含まれています。
デプロイ可能なソリューションとそのインターフェースの例を提供する。
論文 参考訳(メタデータ) (2022-02-25T08:57:06Z) - Safe RAN control: A Symbolic Reinforcement Learning Approach [62.997667081978825]
本稿では,無線アクセスネットワーク(RAN)アプリケーションの安全管理のためのシンボル強化学習(SRL)アーキテクチャを提案する。
我々は、ユーザが所定のセルネットワークトポロジに対して高レベルの論理的安全性仕様を指定できる純粋に自動化された手順を提供する。
ユーザがシステムに意図仕様を設定するのを支援するために開発されたユーザインターフェース(UI)を導入し、提案するエージェントの動作の違いを検査する。
論文 参考訳(メタデータ) (2021-06-03T16:45:40Z) - Neural Network-based Control for Multi-Agent Systems from
Spatio-Temporal Specifications [0.757024681220677]
仕様言語としてSTREL(Spatio-Temporal Reach and Escape Logic)を使用します。
STREL仕様を用いた制御合成問題のマッピングを行い,勾配法と勾配法の組み合わせによる解法を提案する。
我々はオフライン最適化の結果を用いてニューラルネットワークをトレーニングし、制御が現在の状態を入力する機械学習技術を開発した。
論文 参考訳(メタデータ) (2021-04-06T18:08:09Z) - Symbolic Reinforcement Learning for Safe RAN Control [62.997667081978825]
無線アクセスネットワーク(RAN)アプリケーションにおける安全な制御のためのシンボリック強化学習(SRL)アーキテクチャを紹介します。
本ツールでは,LTL(Linear Temporal Logic)で表現された高レベルの安全仕様を選択して,所定のセルネットワーク上で動作しているRLエージェントをシールドする。
ユーザインタフェース(ui)を用いて,ユーザがインテントの仕様をアーキテクチャに設定し,許可されたアクションとブロックされたアクションの違いを検査する。
論文 参考訳(メタデータ) (2021-03-11T10:56:49Z) - Ontological Smart Contracts in OASIS: Ontology for Agents, Systems, and
Integration of Services (Extended Version) [0.7999703756441756]
エージェント・システム・サービス統合のためのオントロジー (Ontology for Agents, Systems, and Integration of Services,略してOasis) と呼ばれる,エージェントとその相互作用をモデル化するためのオントロジーを拡張します。
OSCは、エージェント間の責任と承認を確立するためのスマートコントラクトのオントロジ表現であり、条件付きではエージェントのインタラクションを制限および制限し、エージェントアクションをトリガーするアクティベーションメカニズムを定義し、OSC上の制約とコントラクト用語を定義する。
論文 参考訳(メタデータ) (2020-12-02T18:58:26Z) - SOTER on ROS: A Run-Time Assurance Framework on the Robot Operating
System [5.358161704743753]
SOTERは安全な分散移動ロボットシステムを構築するためのランタイム保証フレームワークである。
我々は、未知のコンポーネントや信頼できないコンポーネントを使用した場合であっても、SOTERを有効にするシステムが安全であることを示す。
論文 参考訳(メタデータ) (2020-08-21T22:48:26Z) - Towards an Interface Description Template for AI-enabled Systems [77.34726150561087]
再利用(Reuse)は、システムアーキテクチャを既存のコンポーネントでインスタンス化しようとする、一般的なシステムアーキテクチャのアプローチである。
現在、コンポーネントが当初目的としていたものと異なるシステムで運用する可搬性を評価するために必要な情報の選択をガイドするフレームワークは存在しない。
我々は、AI対応コンポーネントの主情報をキャプチャするインターフェイス記述テンプレートの確立に向けて、現在進行中の作業について述べる。
論文 参考訳(メタデータ) (2020-07-13T20:30:26Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。