Co-Simulation of Human-Robot Collaboration: from Temporal Logic to 3D Simulation

TL;DR

This paper introduces a co-simulation framework combining formal model checking with 3D simulation to enhance safety verification in human-robot collaboration systems, making formal methods more accessible to safety engineers.

Contribution

It integrates formal verification with 3D simulation for HRC safety analysis, improving usability for safety engineers unfamiliar with formal methods.

Findings

Successful integration of Morse simulator with Zot model checker

Enhanced visualization of hazardous situations in HRC

Improved safety verification process for human-robot systems

Abstract

Human-Robot Collaboration (HRC) is rapidly replacing the traditional application of robotics in the manufacturing industry. Robots and human operators no longer have to perform their tasks in segregated areas and are capable of working in close vicinity and performing hybrid tasks -- performed partially by humans and by robots. We have presented a methodology in an earlier work [16] to promote and facilitate formally modeling HRC systems, which are notoriously safety-critical. Relying on temporal logic modeling capabilities and automated model checking tools, we built a framework to formally model HRC systems and verify the physical safety of human operator against ISO 10218-2 [10] standard. In order to make our proposed formal verification framework more appealing to safety engineers, whom are usually not very fond of formal modeling and verification techniques, we decided to couple our model checking approach with a 3D simulator that demonstrates the potential hazardous situations to the safety engineers in a more transparent way. This paper reports our co-simulation approach, using Morse simulator [4] and Zot model checker [14].