Safety Assessment of Collaborative Robotics Through Automated Formal Verification

A crucial aspect of physical human–robot collaboration (HRC) is to maintain a safe common workspace for human operator. However, close proximity between human–robot and unpredictability of human behavior raises serious challenges in terms of safety. This article proposes a risk analysis methodology for collaborative robotic applications, which is compatible with well-known standards in the area and relies on formal verification techniques to automate the traditional risk analysis methods. In particular, the methodology relies on temporal logic-based models to describe the different possible ways in which tasks can be carried out, and on fully automated formal verification techniques to explore the corresponding state space to detect and modify the hazardous situations at early stages of system design.