  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.
