Formal verification of safety properties of collaborative robotic applications including variability

Michael Rathmair, Christoph Luckeneder, Thomas Haspl, Berhnard Reiterer, Ralph Hoch, Michael Hofbaur, Hermann Kaindl

Publication: Scientific journalConference articlepeer-review

Abstract

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.

Original languageEnglish
Pages (from-to)1283-1288
Number of pages6
Journal2021 30th IEEE International Conference on Robot and Human Interactive Communication, RO-MAN 2021
DOIs
Publication statusPublished - 8 Aug 2021
Externally publishedYes
Event30th IEEE International Conference on Robot and Human Interactive Communication, RO-MAN 2021 - Virtual, Vancouver, Canada
Duration: 8 Aug 202112 Aug 2021

Bibliographical note

Publisher Copyright:
© 2021 IEEE.

Cite this