From Composable Models to Correct-by-Construction Software for Contact-Rich Robotic Mobile-Manipulation Tasks

Software frameworks like the <italic xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">Stack of Tasks</i> (SoT), the Stanford <italic xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">Whole-Body Control</i> (WBC) library, or the <italic xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">instantaneous Task Specification using Constraints</i> (iTaSC) have enabled robots to perform advanced, contact-oriented manipulation tasks. <italic xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">jgeom_constr</i> and <italic xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">eTaSL</i> are among the few formal, computer-interpretable languages that allow users to specify such tasks independent of these frameworks. We analyse these languages for their limitations with respect to <italic xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">composability</i>, the design for extensibility without having to change existing models, and <italic xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">compositionality</i>, meaning that the semantics of compositions unambiguously follows from the semantics of the components and of the composition relations. To overcome these limitations we design a graph-structured and well-defined interchange format for such tasks. The associated tooling enables us to generate correct-by-construction code that adheres to predefined rules and constraints. We showcase our models and toolchain by <italic xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">incrementally</i> constructing a workspace-alignment application for a highly-redundant mobile platform that is equipped with two 7-DoF, torque-controlled manipulators.