Correct-by-Construction Design of Contextual Robotic Missions Using Contracts
Piergiuseppe Mallozzi, Pierluigi Nuzzo, Nir Piterman, Gerardo Schneider, Patrizio Pelliccione
TL;DR
The paper tackles the challenge of robustly specifying and implementing robotic missions across changing contexts by introducing a compositional framework built on assume-guarantee contracts and the Contract-Based Goal Graph (CGG). Each context-driven sub-mission is synthesized into an independent controller, and CROME orchestrates transitions between them to preserve correctness under context switches. Key contributions include the CGG formalism, a timed-automata-based orchestration layer with activation-aware Mealy controllers, and evidence of substantial synthesis-time improvements over monolithic LTL approaches. The approach enables scalable, correct-by-construction contextual missions with practical tooling and demonstrated case-study results, suggesting strong impact for industrial and safety-critical robotic applications.
Abstract
Effectively specifying and implementing robotic missions poses a set of challenges to software engineering for robotic systems. These challenges stem from the need to formalize and execute a robot's high-level tasks while considering various application scenarios and conditions, also known as contexts, in real-world operational environments. Writing correct mission specifications that explicitly account for multiple contexts can be tedious and error-prone. Furthermore, as the number of contexts, and consequently the complexity of the specification, increases, generating a correct-by-construction implementation (e.g., by using synthesis methods) can become intractable. A viable approach to address these issues is to decompose the mission specification into smaller, manageable sub-missions, with each sub-mission tailored to a specific context. Nevertheless, this compositional approach introduces its own set of challenges in ensuring the overall mission's correctness. In this paper, we propose a novel compositional framework for specifying and implementing contextual robotic missions using assume-guarantee contracts. The mission specification is structured in a hierarchical and modular fashion, allowing for each sub-mission to be synthesized as an independent robot controller. We address the problem of dynamically switching between sub-mission controllers while ensuring correctness under predefined conditions.