ROSMonitoring: A Runtime Verification Framework for ROS

2 min read

ROSMonitoring adds runtime verification to ROS without tying it to one specification language. A YAML file names the topics to watch and the message types; a generator then writes monitor nodes in Python and rewires the launch files so traffic passes through them. Monitors hand each intercepted message, serialised as JSON, to a separate oracle that holds the property (the follow-up paper lists past-time LTL, MTL and STL oracles) and returns a verdict. Offline monitors only log. Online monitors either log the verdict and publish a warning, or filter: they drop messages that would violate the property, so the property is enforced on the topic.

I only saw the abstract and the description of the framework in its follow-up, ROSMonitoring 2.0 (Ghaffari Saadat, Ferrando, Dennis and Fisher, FMAS 2024).

Findings

  • The abstract stresses portability across ROS distributions and independence from the specification formalism.
  • It is demonstrated on a simulation of the Mars Curiosity rover, with experiments on how it scales. I did not see the numbers.

Limits

  • Per the follow-up paper, the original framework monitors topics only (no ROS services) and orders events by when subscribers receive them, which can scramble the order across several topics.
  • A filtering monitor sits in the message path, so its latency and failure become the system’s.
  • Dropping a violating message is the only built-in reaction. What the robot should do instead is left to the developer.

Relevance

The filter mode is a tiny shield for ROS topics; compare shield synthesis and Simplex. The verdict semantics come from Leucker and Schallhart and Bauer et al.. The tool shows up as an exemplar in the ROS RV guidelines; see runtime monitoring.