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

The runtime veriication of multi-domain software applications implementing the behaviors of modern robots is a challenging task. On the one hand, assertion-based veriication (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 veriication. 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.