Run-Time Requirement Enforcement of Safety Requirements of Human-Robot Interactions

Human-robot interaction (HRI) is characterized by a close collaboration between robots and humans and thus comes with a set of safety requirements on the robot execution that need to be guaranteed throughout this interaction. Several techniques have been proposed to specify the correct behavior of a robot that interacts with a human. The majority of them simulate the interaction in order to validate that the system is executing as specified. However, simulation is not enough to guarantee the safe behavior of a robot in presence of the uncertainty typically given by human behavior. In this paper, we suggest to apply runtime requirement enforcement (RRE) techniques using finite state machines (FSMs) to enforce a given set of safety requirements related to the interaction between a human and a robot, such as collision avoid-ance. We then suggest to apply formal verification techniques, i.e., probabilistic model checking to verify the probability of different safety requirements on two HRI scenarios. In addition, an analysis of the verification times is presented.