Monitoring ROS2: from Requirements to Autonomous Robots

TL;DR

This paper presents a formal, automated method for generating runtime monitors from natural language requirements for ROS2 autonomous robots, enhancing safety and reducing manual effort in complex robotic systems.

Contribution

It introduces an integrated framework combining FRET, Copilot, and Ogma to automatically generate ROS2-compatible runtime monitors from structured natural language requirements.

Findings

Automated translation of requirements into temporal logic formulas.

Generation of ROS2 packages for monitoring nodes.

Facilitated integration of monitors into ROS2 systems.

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.