Safety assurance of autonomous agricultural robots: from offline model-checking to runtime verification

摘要

The ongoing efforts to deploy safety-critical autonomous robots that operate in semi-structured, dynamic, and uncertain environments, reinforce the importance of supplementing traditional risk-management activities, input-based testing, and quality assurance procedures, with formal verification methods. With this approach, one may guarantee safe behavior in all relevant scenarios. In this paper, we propose a safety assurance framework enabling the integrated use of formal verification at all stages of the engineering life-cycle, beginning at the concept study, design, development, deployment, and operation. Along the way, a real use case from the agricultural industry, namely robotic ultra-violet (UVC) plant treatment, is used to demonstrate the proposed methodology. In particular, the transfer of offline model-checking artifacts to Runtime Verification elucidates how safety requirements can be conceptualized and subsequently translated into online monitors that are integrated seamlessly with the robot’s control system. Our study elaborates on the modeling and verification process, and on the accompanying monitoring tool chain that facilitates the integration in ROS2 applications.