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

Publikation: Wissenschaftliche FachzeitschriftKonferenzartikelBegutachtung

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.

OriginalspracheEnglisch
Seiten (von - bis)1283-1288
Seitenumfang6
Fachzeitschrift2021 30th IEEE International Conference on Robot and Human Interactive Communication, RO-MAN 2021
DOIs
PublikationsstatusVeröffentlicht - 8 Aug. 2021
Extern publiziertJa
Veranstaltung30th IEEE International Conference on Robot and Human Interactive Communication, RO-MAN 2021 - Virtual, Vancouver, Kanada
Dauer: 8 Aug. 202112 Aug. 2021

Bibliographische Notiz

Publisher Copyright:
© 2021 IEEE.

Zitat