From Composable Models to Correct-By-Construction Software for Contact-Rich Robotic Mobile-Manipulation Tasks
Sven Schneider, Vamsi Krishna Kalagaturu, Herman Bruyninckx, Nico Hochgeschwender
Abstract
Software frameworks like the Stack of Tasks (SoT), the Stanford Whole-Body Control (WBC) library, or the instantaneous Task Specification using Constraints (iTaSC) have enabled robots to perform advanced, contact-oriented manipulation tasks. jgeom constr and eTaSL 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 composability, the design for extensibility without having to change existing models, and compositionality, 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 incrementally constructing a workspace-alignment application for a highly-redundant mobile platform that is equipped with two 7-DoF, torque-controlled manipulators.