A Verification Methodology for Safety Assurance of Robotic Autonomous Systems

TL;DR

This paper tackles safety assurance for robotic autonomous systems operating in dynamic, human-shared agricultural environments by proposing an integrated verification methodology that spans from concept through operation. The approach combines hazard analysis, formal modelling with RoboChart and $tock$-CSP, probabilistic model checking via PRISM, and runtime verification with monitors generated from formal specifications, all focused on a field UVC-treatment robot. A key contribution is the formal modelling and verification of a Safety Controller, demonstrated in a real-world agricultural setting, showing early issue detection and alignment with $SIL$ targets while enabling iterative improvement through runtime data. The methodology supports lifecycle-wide safety assurance aligned with standards, offering a practical path to safer autonomous agricultural systems and scalable verification for complex RAS.

Abstract

Autonomous robots deployed in shared human environments, such as agricultural settings, require rigorous safety assurance to meet both functional reliability and regulatory compliance. These systems must operate in dynamic, unstructured environments, interact safely with humans, and respond effectively to a wide range of potential hazards. This paper presents a verification workflow for the safety assurance of an autonomous agricultural robot, covering the entire development life-cycle, from concept study and design to runtime verification. The outlined methodology begins with a systematic hazard analysis and risk assessment to identify potential risks and derive corresponding safety requirements. A formal model of the safety controller is then developed to capture its behaviour and verify that the controller satisfies the specified safety properties with respect to these requirements. The proposed approach is demonstrated on a field robot operating in an agricultural setting. The results show that the methodology can be effectively used to verify safety-critical properties and facilitate the early identification of design issues, contributing to the development of safer robots and autonomous systems.

Figures (4)

• Figure 1: Overview of the verification methodology across the engineering lifecycle. Iterative steps allow returning to the relevant previous phase based on the failure’s root cause. All artifacts shown have been produced and exemplified in our agricultural case study.
• Figure 2: The robot was deployed in a polytunnel for simulated UVC operation.
• Figure 3: Overview of the RoboChart model of the SIS architecture, generated using RoboTool.
• Figure 4: State machines defining the safety response logic for UVC control, speed management, and alerting (sound).