Marcus Pirron

• Modern robotic applications consist of a variety of robotic systems that work together to achieve complex tasks. Programming these applications draws from multiple fields of knowledge and typically involves low-level imperative programming languages that provide little to no support for abstraction or reasoning. We present a unifying programming model, ranging from automated controller synthesis for individual robots to a compositional reasoning framework for inter-robot coordination. We provide novel methods on the topics of control and planning of modular robots, making contributions in three main areas: controller synthesis, concurrent systems, and verification. Our method synthesizes control code for serial and parallel manipulators and leverages physical properties to synthesize sensing abilities. This allows us to determine parts of the system’s state that previously remained unmeasured. Our synthesized controllers are robust; we are able to detect and isolate faulty parts of the system, find alternatives, and ensure continued operation. On the concurrent systems side, we deal with dynamic controllers affecting the physical state, geometric constraints on components, and synchronization between processes. We provide a programming model for robotics applications that consists of assemblies of robotic components together with a run-time and a verifier. Our model combines message-passing concurrent processes with motion primitives and explicit modeling of geometric frame shifts, allowing us to create composite robotic systems for performing tasks that are unachievable for individual systems. We provide a verification algorithm based on model checking and SMT solvers that statically verifies concurrency-related properties (e.g. absence of deadlocks) and geometric invariants (e.g. collision-free motions). Our method ensures that jointly executed actions at end-points are communication-safe and deadlock-free, providing a compositional verification methodology for assemblies of robotic components with respect to concurrency and dynamic invariants. Our results indicate the efficiency of our novel approach and provide the foundation of compositional reasoning of robotic systems.
• Moderne Roboteranwendungen bestehen aus einer Vielzahl von Robotersystemen, die zur Bewältigung komplexer Aufgaben zusammenarbeiten. Die Programmierung dieser Anwendungen bedient sich einer Vielzahl von Wissensgebieten und stützt sich üblicherweise auf einfache imperative Programmiersprachen, die wenig bis keine Unterstützung für Abstraktion oder Beweisbarkeit bieten. Wir stellen ein vereinheitlichendes Programmiermodell vor, welches von der automatisierten Steuerungssynthese für einzelne Roboter bis hin zu einem kompositorischen Argumentationsrahmen für die Koordination zwischen Robotern reicht. Unter Verwendung modularer Roboter entwickeln wir neuartige Methoden in drei Bereichen: Controllersynthese, nebenläufige Systeme und Verifikation. Unsere Methode synthetisiert Steuerungscode für serielle und parallele Roboter und nutzt physikalische Eigenschaften, um durch intelligente Sensorlösungen Fähigkeiten und Flexibilität dieser Systeme zu verbessern. Unsere synthetisierten Steuerungen sind robust: Fehlerhafte Teile des Systems können erkannt und isoliert sowie Alternativen zu diesen gefunden werden, um den weiteren Betrieb sicherzustellen; ebenso können wir zuvor nicht bestimmbare Teile des Systemzustands messen. Unser Modell kombiniert nebenläufige Prozesse mit atomaren Bewegungseinheiten und der expliziten Überführung jeweiliger Ortskoordinatensysteme. Die auf diese Weise erzeugten Robotersysteme eignen sich für die Ausführung von Aufgaben, die für Einzelsysteme unausführbar sind. Wir stellen einen auf Modellprüfung und SMT-Solvern basierenden Verifikationsalgorithmus bereit, der nebenläufigkeitsbezogene Eigenschaften (z. B. das Fehlen von Deadlocks) und geometrische Invarianten (z. B. kollisionsfreie Bewegungen) statisch verifiziert. Dadurch ist gewährleistet, daß gemeinsam ausgeführte Aktionen an Endpunkten kommunikationssicher und deadlock-frei sind. Unsere Resultate belegen die Effizienz unseres neuartigen Ansatzes und bilden die Grundlage für die kompositorische Beweisbarkeit von Robotersystemen.