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

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.