A Formal Verification Approach for Robot Workflows

Publikation aus Robotics

Michael Rathmair, Thomas Haspl, Titanilla Komenda, Bernhard Reiterer, Michael Hofbaur

20th International Conference on Advanced Robotics (ICAR), Ljubljana, Slovenia , 12/2021


Formal verification is a powerful tool to show functional correctness of task and workflow descriptions representing robot-based manufacturing processes. A prerequisite is the integration of the process into a well-structured modeling and design architecture. In this paper, we propose a layer-based formal verification scheme that accepts BPMN-based input models. The integrated composition of tools enables state-space comprehensive verification targeting a set of user-defined verification goals. The importance of formal verification scheme is highlighted by our methodology which strictly supports a model refinement and abstraction approach. Since the complexity and size of robot application process models are steadily increasing this feature in combination with a clear verification methodology is a substantial contribution towards industrial acceptance.

Keywords: Manufacturing processes, Service robots, Complexity theory, Task analysis, Formal verification

Url: doi: 10.1109/ICAR53236.2021.9659366