Runtime verification of robotic applications inspecting radioactive environments

The growing reliance on robotics with respect to various hazardous applications has created the need for robust and reliable robotic systems, particularly when inspecting radioactive environments. These inspections inherently demand a high degree of safety and accuracy, as they often involve working in close proximity to harmful materials.

Runtime verification (RV) refers to the process of continuously observing and analysing the behaviour of a system during execution to ensure that it constantly adheres to specified properties. Utilising RV facilitates detecting potential violations, inconsistencies, or even failures in the system’s operation, thus providing consistent feedback. An important property that is monitored consistently is the sensor’s readings, establishing thresholds for radiation levels in order to trigger alarms, should the limits be exceeded.

The open-source framework ROSMonitoring is developed to facilitate the RV of robotic systems based on ROS (Robot Operating System). Customised monitors were integrated by instrumentation of .yaml files, where the monitors would be able to intercept messages in real time and verify the data of these messages by sending them in JSON format to the Oracle. These were subsequently verified against a set of properties, defined by temporal logic. This process would allow developers to monitor their robotic systems in real time, ensuring that specified requirements are being met and identifying potential issues before bringing about catastrophic consequences.

A radiation simulation plugin was used in order to allow the accurate and controlled modelling and testing of robotic systems by simulating radiation exposure. This plugin enables the testing and validation of robotic applications under varied settings, without subjecting the actual system or workers to potentially dangerous materials. With the use of this plugin, the inspection of radioactive environments could be simulated with precision.

Figure 1. High-level overview of ROSMonitoring

Figure 2. Gazebo representation of the nuclear facility at Sellafield to be inspected

Student: Miriana Drago

Supervisor : Dr Christian Colombo