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.
翻译:我们提出了一个工具支持的方法,用于综合、核查和验证在使用合作机器人的制造过程中负责人-机器人互动安全的控制软件。在人-机器人协作中,使用软件安全控制器来改进操作安全,例如,触发停机机制或紧急停机以避免事故。复杂的机器人任务和日益密切的人类-机器人互动对控制开发者和验证当局提出了新的挑战。这些挑战中的关键是,必须确保安全控制器在明确(而且最好是薄弱)假设下正确无误。我们的控制器综合、核查和验证方法以目标应用的程序、风险分析及相关安全条例为依据。根据一套最佳性标准,从可行的控制器的设计空间中挑选控制器,根据正确性标准进行正式核查,并转化为可执行的代码,并在数字双方面得到验证。因此,控制器能够发现危险发生的情况,将程序转移到安全状态,并在某些情况下,将程序恢复到操作状态,从而可以恢复其最初的任务。我们通过一个涉及软件安全开发的案例研究,展示了我们的软件制造控制器的合作性工作的有效性。