Verified Synthesis of Optimal Safety Controllers for Human-Robot Collaboration

TY - JOUR

T1 - Verified Synthesis of Optimal Safety Controllers for Human-Robot Collaboration

AU - Gleirscher, Mario

AU - Calinescu, Radu

AU - Douthwaite, James

AU - Lesage, Benjamin Michael Jean-Rene

AU - Paterson, Colin

AU - Aitken, Jonathan

AU - Alexander, Rob

AU - Law, James

N1 - © 2022 The Author(s). Published by Elsevier B.V.

PY - 2022/4/4

Y1 - 2022/4/4

N2 - We present a tool-supported approach to the synthesis, verification, and testing of the control software responsible for the safety of human-robot interaction in manufacturing processes that use collaborative robots. In human-robot collaboration, software-based safety controllers are used to improve operational safety, for example, by triggering shutdown mechanisms or emergency stops to reduce the likelihood of 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 integrated synthesis, verification, and test 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 tested in a digital twin. The resulting controller can detect the occurrence of hazards, move the process into a safe state, and, under 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.

AB - We present a tool-supported approach to the synthesis, verification, and testing of the control software responsible for the safety of human-robot interaction in manufacturing processes that use collaborative robots. In human-robot collaboration, software-based safety controllers are used to improve operational safety, for example, by triggering shutdown mechanisms or emergency stops to reduce the likelihood of 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 integrated synthesis, verification, and test 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 tested in a digital twin. The resulting controller can detect the occurrence of hazards, move the process into a safe state, and, under 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.

KW - software engineering

KW - controller synthesis

KW - formal verification

KW - probabilistic model checking

KW - code generation

KW - risk modelling

KW - human-robot collaboration

KW - cobot safety

KW - manufacturing automation

KW - digital twin

U2 - 10.1016/j.scico.2022.102809

DO - 10.1016/j.scico.2022.102809

M3 - Article

SN - 0167-6423

JO - Science of Computer Programming

JF - Science of Computer Programming

M1 - 102809

ER -