Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Safety Controller Synthesis for Collaborative Robots

Mario Gleirscher, Radu Calinescu

TL;DR

This work tackles the problem of synthesizing safe, correct-by-construction automatic safety controllers (ASCs) for collaborative robots in manufacturing. It proposes an end-to-end pipeline that models the process and safety risks as a Markov decision process (MDP), translates risk structures into guarded commands via the Yap tool, and uses PRISM to verify and synthesize optimal policies under multi-criteria objectives. The approach is demonstrated on a running cobot welding cell, showing that multiple hazards and mitigation options can be incorporated and that the resulting policies achieve high accident-freedom while exposing trade-offs with productivity and nuisance. By providing formal verification and a traceable design workflow, the method supports robust ASC assurance claims in human-robot collaboration settings.

Abstract

In human-robot collaboration (HRC), software-based automatic safety controllers (ASCs) are used in various forms (e.g. shutdown mechanisms, emergency brakes, interlocks) to improve operational safety. Complex robotic tasks and increasingly close human-robot interaction pose new challenges to ASC developers and certification authorities. Key among these challenges is the need to assure the correctness of ASCs under reasonably weak assumptions. To address this need, we introduce and evaluate a tool-supported ASC synthesis method for HRC in manufacturing. Our ASC synthesis is: (i) informed by the manufacturing process, risk analysis, and regulations; (ii) formally verified against correctness criteria; and (iii) selected from a design space of feasible controllers according to a set of optimality criteria. The synthesised ASC 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.

Safety Controller Synthesis for Collaborative Robots

TL;DR

This work tackles the problem of synthesizing safe, correct-by-construction automatic safety controllers (ASCs) for collaborative robots in manufacturing. It proposes an end-to-end pipeline that models the process and safety risks as a Markov decision process (MDP), translates risk structures into guarded commands via the Yap tool, and uses PRISM to verify and synthesize optimal policies under multi-criteria objectives. The approach is demonstrated on a running cobot welding cell, showing that multiple hazards and mitigation options can be incorporated and that the resulting policies achieve high accident-freedom while exposing trade-offs with productivity and nuisance. By providing formal verification and a traceable design workflow, the method supports robust ASC assurance claims in human-robot collaboration settings.

Abstract

In human-robot collaboration (HRC), software-based automatic safety controllers (ASCs) are used in various forms (e.g. shutdown mechanisms, emergency brakes, interlocks) to improve operational safety. Complex robotic tasks and increasingly close human-robot interaction pose new challenges to ASC developers and certification authorities. Key among these challenges is the need to assure the correctness of ASCs under reasonably weak assumptions. To address this need, we introduce and evaluate a tool-supported ASC synthesis method for HRC in manufacturing. Our ASC synthesis is: (i) informed by the manufacturing process, risk analysis, and regulations; (ii) formally verified against correctness criteria; and (iii) selected from a design space of feasible controllers according to a set of optimality criteria. The synthesised ASC 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.

Paper Structure

This paper contains 18 sections, 7 equations, 14 figures, 4 tables.

Table of Contents

  1. Introduction
  2. Related Work
  3. Running Example: Manufacturing Cobots
  4. Preliminaries
  5. Approach: Safety Controller Synthesis
  6. Modelling the Manufacturing Process
  7. Safety Analysis and Risk Modelling
  8. Designing Mitigation and Resumption Options
  9. Verified Controller Synthesis
  10. Guarded Command Generation
  11. MDP Verification
  12. Policy Synthesis
  13. DTMC Verification
  14. Evaluation
  15. Research Questions and Evaluation Methodology
  16. ...and 3 more sections

Figures (14)

  • Figure 1: Actual (a, b) and replicated (c) cobot setting
  • Figure 2: Conceptual setting (a) and activities in the manufacturing process (b) performed by the operator, the robot, and the welder (in blue), classified by the activity groups moving and base (in gray)
  • Figure 3: Main and of the proposed method (future work indicated in dashed lines)
  • Figure 4: Fragment of the data type definition in PRISM
  • Figure 5: PRISM model fragment of the module robotArm
  • ...and 9 more figures

Theorems & Definitions (2)

  • Definition 1
  • Definition 2