Software Toolchain for Modeling and Transforming Robotic Workflows into Formally Verifiable Model Representations

Publikation aus Robotics

Thomas Haspl, Michael Rathmair, Maximilian Papa, Michael Hofbaur , Andrea M. Tonello

Proceedings of the ARW 2022, Villach , 6/2022


Formal verification represents an essential concept of mathematically proving or disproving the correctness of a system based on previously defined specifications. Applied to robotic workflows it can be used to prove their functional correctness, where it gains particular importance with the introduction of robot programming types for non-experts. In this paper, a software toolchain for modeling and transforming robotic workflows into formally verifiable model representations is presented. A graphical way of modeling robotic workflows in a distinctive way with a subsequent automatic transformation into verifiable code form the core of the presented toolchain. A software for generating formal specifications based on a modelled robotic workflow completes the toolchain presented in this work. The output artifacts of the particular software parts eventually allow a formal verification of robotic workflows against a desired behavior represented by the generated specifications.

Keywords: Formal verification, model checking, automatic model transformation, robotic systems, industrial robotic workflows