ROS Monitoring

ROSMonitoring is a framework to support runtime verification of robotic applications developed using the Robot Operating System (ROS). The main advantages of ROSMonitoring compared to the state-of-the-art are its portability across multiple ROS distributions and its agnosticism with respect to the specification formalism. It creates monitors that are placed between ROS nodes to intercept messages on relevant topics and check the events generated by these messages against formally specified properties.

ROSMonitoring has been used in different scenarios inside RAIN to verify robot compliance at runtime.

ROSMonitoring is useful for industry because it allows a high-level way to verify ROS-based systems at runtime. With respect to other formal verification techniques, Runtime Verification does not need to abstract nor model the system. ROSMonitoring can be applied even when the system under analysis is considered a black box: this aspect makes ROSMonitoring easily usable by users with no experience in formal verification. Since ROS is the de facto standard for developing robotic solutions both in academia and industry, ROSMonitoring is highly compatible for existing and future applications.