Edge-Cloud Orchestration of Assertion-Based Monitors for Robotic Applications

The runtime verification of multi-domain software applications implementing the behaviors of modern robots is a challenging task. On the one hand, assertion-based verification (ABV) has shown great potential to check the correctness of complex systems at runtime. On the other hand, the computational overhead introduced by runtime ABV can be substantial, variable and non-deterministic. As a consequence, applying accurate ABV at runtime to autonomous robots, which are often characterized by resource-constrained computing architectures, can lead to severe slowdowns of the software execution and failures of temporal constraints, thus compromising the overall system’s correctness. We address this challenge by proposing a platform for runtime ABV that implements monitor synthesis from signal temporal logic assertions and dynamic monitor migration across edge devices and the cloud. The synthesized monitors are wrapped into ROS-compliant nodes and connected to the system under verification. The overall ABV framework and the related migration mechanism are then containerized with Docker for both edge and cloud computing. To evaluate the proposed platform, we present the results obtained with a set of synthetic benchmarks and with an industrial case study, which implements the mission of a Robotnik RB-Kairos mobile robot in a smart manufacturing production line. Note to Practitioners . This article was motivated by the need for accurate and runtime verification of robotic systems software. Verification and validation of intelligent systems are often incomplete, as they cannot anticipate all potential scenarios, including errors or unexpected events. On top of this, assertion-based verification can also be resource-intensive; therefore, careful use of resources is required to avoid overloading the robot’s computational resources with the monitors. To achieve this, we used signal temporal logic, a widely accepted solution to monitor robotic and distributed applications. The main contribution of this work is a framework that can automatically synthesize the monitors that interface with the Robot Operating System (ROS) and also the capability of optimizing the end-to-end latency of verification at runtime by exploiting a distributed computing architecture (i.e., edge-cloud). In future work, we will address not only the minimization of end-to-end latency but also the timing upper bound of monitors to achieve runtime deterministic verification.