論文の概要: 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によって、実行可能モニタに自動的に変換できます。
我々は,核施設の遠隔検査に携わる自律ローバーの仕様と検証を通じて,我々のアプローチを説明し,我々のフレームワークの他の有用な特徴を示す小さな例で仕上げる。
関連論文リスト
- Complex Event Recognition with Symbolic Register Transducers: Extended Technical Report [51.86861492527722]
本稿では,オートマトンに基づく複合イベント認識システムを提案する。
本システムは,記号とレジスタオートマトンを組み合わせたオートマトンモデルに基づいている。
我々は、イベントストリーム上のパターンを検出するために、SRTをCERでどのように使用できるかを示す。
論文 参考訳（メタデータ） (2024-07-03T07:59:13Z) - ROS-LLM: A ROS framework for embodied AI with task feedback and structured reasoning [74.58666091522198]
非専門家による直感的なロボットプログラミングのためのフレームワークを提案する。
ロボットオペレーティングシステム(ROS)からの自然言語のプロンプトと文脈情報を活用する
我々のシステムは,大規模言語モデル (LLM) を統合し,非専門家がチャットインタフェースを通じてシステムにタスク要求を記述できるようにする。
論文 参考訳（メタデータ） (2024-06-28T08:28:38Z) - Protocols to Code: Formal Verification of a Next-Generation Internet Router [9.971817718196997]
SCIONルータは、敵の環境でセキュアなパケット転送のための暗号化プロトコルを実行する。
プロトコルのネットワーク全体のセキュリティ特性と,その実装の低レベル特性の両方を検証する。
本稿では,本研究のアプローチを説明し,主な成果を要約し,検証可能なシステムの設計と実装に関する教訓を抽出する。
論文 参考訳（メタデータ） (2024-05-09T19:57:59Z) - 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) - 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) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。