A Formal Verification Approach for Robot Workflows

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.