Monitoring ROS2: from Requirements to Autonomous Robots

• URL: http://arxiv.org/abs/2209.14030v1
• Date: Wed, 28 Sep 2022 12:19:13 GMT
• Title: Monitoring ROS2: from Requirements to Autonomous Robots
• Authors: Ivan Perez (KBR at NASA Ames Research Center), Anastasia Mavridou (KBR at NASA Ames Research Center), Tom Pressburger (NASA Ames Research Center), Alexander Will (Virginia Commonwealth University), Patrick J. Martin (Virginia Commonwealth University)
• Abstract summary: This paper provides an overview of a formal approach to generating runtime monitors for autonomous robots from requirements written in a structured natural language. Our approach integrates the Formal Requirement Elicitation Tool (FRET) with Copilot, a runtime verification framework, through the Ogma integration tool.
• Score: 58.720142291102135
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Runtime verification (RV) has the potential to enable the safe operation of safety-critical systems that are too complex to formally verify, such as Robot Operating System 2 (ROS2) applications. Writing correct monitors can itself be complex, and errors in the monitoring subsystem threaten the mission as a whole. This paper provides an overview of a formal approach to generating runtime monitors for autonomous robots from requirements written in a structured natural language. Our approach integrates the Formal Requirement Elicitation Tool (FRET) with Copilot, a runtime verification framework, through the Ogma integration tool. FRET is used to specify requirements with unambiguous semantics, which are then automatically translated into temporal logic formulae. Ogma generates monitor specifications from the FRET output, which are compiled into hard-real time C99. To facilitate integration of the monitors in ROS2, we have extended Ogma to generate ROS2 packages defining monitoring nodes, which run the monitors when new data becomes available, and publish the results of any violations. The goal of our approach is to treat the generated ROS2 packages as black boxes and integrate them into larger ROS2 systems with minimal effort.

Related papers

• Runtime Verification via Rational Monitor with Imperfect Information [2.7323347531070974]
  Traditional verification assumes perfect information, meaning the monitoring component perceives everything accurately. This assumption often fails, especially with autonomous systems operating in real-world environments. We extend standard RV of Linear Temporal Logic properties to accommodate scenarios where the monitor has imperfect information and behaves rationally.
  arXiv  Detail & Related papers  (2024-08-21T13:56:06Z)
• Compromising Embodied Agents with Contextual Backdoor Attacks [69.71630408822767]
  Large language models (LLMs) have transformed the development of embodied intelligence. This paper uncovers a significant backdoor security threat within this process. By poisoning just a few contextual demonstrations, attackers can covertly compromise the contextual environment of a black-box LLM.
  arXiv  Detail & Related papers  (2024-08-06T01:20:12Z)
• ROS-LLM: A ROS framework for embodied AI with task feedback and structured reasoning [74.58666091522198]
  We present a framework for intuitive robot programming by non-experts. We leverage natural language prompts and contextual information from the Robot Operating System (ROS) Our system integrates large language models (LLMs), enabling non-experts to articulate task requirements to the system through a chat interface.
  arXiv  Detail & Related papers  (2024-06-28T08:28:38Z)
• Monitoring Unmanned Aircraft: Specification, Integration, and Lessons-learned [3.2248482136498433]
  This paper reports on the integration of runtime monitoring into fully-electric aircraft designed by Volocopter. The correct operation of the monitor is critical for the safety of the aircraft. We have used the stream-based monitoring framework RTLola to generate monitors for a range of requirements.
  arXiv  Detail & Related papers  (2024-04-18T09:42:24Z)
• Large Language Models as General Pattern Machines [64.75501424160748]
  We show that pre-trained large language models (LLMs) are capable of autoregressively completing complex token sequences. Surprisingly, pattern completion proficiency can be partially retained even when the sequences are expressed using tokens randomly sampled from the vocabulary. In this work, we investigate how these zero-shot capabilities may be applied to problems in robotics.
  arXiv  Detail & Related papers  (2023-07-10T17:32:13Z)
• A Compositional Approach to Verifying Modular Robotic Systems [1.385411134620987]
  This paper describes a compositional approach to specifying the nodes in robotic systems built using the Robotic Operating System (ROS) 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.
  arXiv  Detail & Related papers  (2022-08-10T18:01:40Z)
• SABER: Data-Driven Motion Planner for Autonomously Navigating Heterogeneous Robots [112.2491765424719]
  We present an end-to-end online motion planning framework that uses a data-driven approach to navigate a heterogeneous robot team towards a global goal. We use model predictive control (SMPC) to calculate control inputs that satisfy robot dynamics, and consider uncertainty during obstacle avoidance with chance constraints. recurrent neural networks are used to provide a quick estimate of future state uncertainty considered in the SMPC finite-time horizon solution. A Deep Q-learning agent is employed to serve as a high-level path planner, providing the SMPC with target positions that move the robots towards a desired global goal.
  arXiv  Detail & Related papers  (2021-08-03T02:56:21Z)
• Monitoring and Diagnosability of Perception Systems [21.25149064251918]
  We propose a mathematical model for runtime monitoring and fault detection and identification in perception systems. We demonstrate our monitoring system, dubbed PerSyS, in realistic simulations using the LGSVL self-driving simulator and the Apollo Auto autonomy software stack.
  arXiv  Detail & Related papers  (2020-11-11T23:03:14Z)
• Risk-Averse MPC via Visual-Inertial Input and Recurrent Networks for Online Collision Avoidance [95.86944752753564]
  We propose an online path planning architecture that extends the model predictive control (MPC) formulation to consider future location uncertainties. Our algorithm combines an object detection pipeline with a recurrent neural network (RNN) which infers the covariance of state estimates. The robustness of our methods is validated on complex quadruped robot dynamics and can be generally applied to most robotic platforms.
  arXiv  Detail & Related papers  (2020-07-28T07:34:30Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.