Verified Synthesis of Optimal Safety Controllers for Human-Robot Collaboration

TL;DR

The paper tackles the challenge of creating safe, productive human–robot collaboration in manufacturing by presenting a tool-supported, risk-informed workflow for synthesizing, verifying, and validating safety controllers. It models the application as an $MDP$ (and in the enhanced setting as a $pDTMC$) to generate a design space of controllers, then uses probabilistic model checking ($PRISM$) and evoChecker to obtain optimal policies under safety constraints expressed in $PCTL$, while also translating the results to executable code for a digital twin-based validation platform. Key contributions include refined process and risk modelling, integration of stochastic verification with design-space generation, automatic code generation for a digital twin, and a detailed running example demonstrating improved accident-freedom and useful trade-offs between risk and productivity. The work provides a practical, end-to-end approach that links formal verification with runtime validation, potentially strengthening controller assurance and facilitating compliance with cobot safety standards such as ISO 15066. The results indicate that risk-informed safety controllers can mitigate hazards more effectively than stop-only strategies, while enabling safer resumption and higher process utility in a realistic digital-twin environment.

Abstract

We present a tool-supported approach for the synthesis, verification and validation of the control software responsible for the safety of the human-robot interaction in manufacturing processes that use collaborative robots. In human-robot collaboration, software-based safety controllers are used to improve operational safety, e.g., by triggering shutdown mechanisms or emergency stops to avoid accidents. Complex robotic tasks and increasingly close human-robot interaction pose new challenges to controller developers and certification authorities. Key among these challenges is the need to assure the correctness of safety controllers under explicit (and preferably weak) assumptions. Our controller synthesis, verification and validation approach is informed by the process, risk analysis, and relevant safety regulations for the target application. Controllers are selected from a design space of feasible controllers according to a set of optimality criteria, are formally verified against correctness criteria, and are translated into executable code and validated in a digital twin. The resulting controller can detect the occurrence of hazards, move the process into a safe state, and, in certain circumstances, return the process to an operational state from which it can resume its original task. We show the effectiveness of our software engineering approach through a case study involving the development of a safety controller for a manufacturing work cell equipped with a collaborative robot.

Figures (22)

• Figure 1: Work cell concept (a) and activities in the manufacturing process (b) performed by the operator, the robot, and the spot welder, classified by the activity groups moving and base (in light gray)
• Figure 2: Actual (a, b) and replicated (c) work cell with cobot
• Figure 3: Stages of the proposed approach to safety controller synthesis
• Figure 4: Overview of the work steps and artifacts of the process modelling stage
• Figure 5: Execution from the viewpoint of the safety controller. The execution is coordinated by passing a single token between two groups of actors (dashed arcs) performing actions in the process. The controller can perform an update or issue control inputs to the process after every atomic event occurring in the process.

Theorems & Definitions (2)

• Definition 1
• Definition 2