Formal Verification of Safety Properties of Collaborative Robotic Applications including Variability
Publication from Robotics
Michael Rathmair, Christoph Luckeneder, Thomas Haspl, Bernhard Reiterer, Ralph Hoch, Michael Hofbaur, Hermann Kaindl
30th IEEE International Conference on Robot Human Interactive Communication (RO-MAN), pp. 1283-1288 , 8/2021
Formal design verification receives increased importance since the complexity of safety-critical technical applications steadily increases. In this paper, we describe an approach for symbolic model checking of collaborative robotic systems against safety properties. In particular, the methodology presented enables verification even under system modifications and adaptive behavior generally represented as variability. Architectural, behavioral and environmental models are correspondingly abstracted to reach a balance of generality and verifiability with reasonable effort. To demonstrate the proposed method, we use the model of a collaborative assembly use case and formally verify the existence of mechanical clamping hazards between the robot’s moving end effector and static environment objects.
Keywords: Robotic assembly, Adaptation models, Collaboration, Model checking, Hazards, Clamps, Collision avoidance