Issue link: https://htpgraphics.uberflip.com/i/1385717
VERIFICATION & VALIDATION RAIN PROGRESS // ROSMonitoring has been used in different scenarios inside RAIN to verify robot compliance at runtime and demonstrates a collaboration between the RAIN and ORCA Hubs. ROSMonitoring is available at https://github.com/ autonomy-and-verification-uol/ROSMonitoring. It has been used to formally verify various robots, such as Jackal, Husky, Mars Curiosity rover, and Gantry- type robots. With ROSMonitoring, monitors can be synthesised automatically. The user only needs to specify the formal property to verify, and where the monitors can gather the information to check it (ROS topics). UNIQUENESS // By adding runtime monitors to existing robotic software, we can ensure the system will behave during runtime. The monitors in fact can be used both to passively observe/judge the system, and to enforce the correct behaviour. ROSMonitoring is a framework to support Runtime Verification (RV) of robotic applications developed using the Robot Operating System (ROS). 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. With ROSMonitoring, for instance, it is possible to correct unexpected system execution by filtering out incorrect communication messages. The key aspect of Runtime Verification is its being lightweight and easy to apply. It is not required to model any abstraction of the system, and it can be deployed directly to check the actual code. Its similarities with testing make it a powerful ally from an engineering perspective. FUTURE ASPIRATIONS // There are many opportunities for ROSMonitoring, and for Runtime Verification in general in the context of robotics applications. We are planning to keep working on ROSMonitoring, in particular by extending it and by applying it to new and challenging scenarios. We will look to exploit its main advantages, compared to the state of the art, which are its; - portability across multiple ROS distributions and its - agnosticism w.r.t. the specification formalism. Additionally, ROSMonitoring is useful for industry because it allows a high-level way to verify ROS-based systems at runtime. 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 a common software for developing robotic solutions both in academia and industry, ROSMonitoring is highly compatible for existing and future applications. 25