Correct-by-Construction Design of Contextual Robotic Missions Using Contracts

TL;DR

This paper introduces a compositional framework using assume-guarantee contracts for designing and implementing robotic missions that adapt to various contexts, ensuring correctness through hierarchical and modular specifications.

Contribution

It presents a novel hierarchical, modular approach for specifying and synthesizing context-aware robotic missions with dynamic switching capabilities.

Findings

Framework enables correct dynamic context switching.

Hierarchical specifications improve manageability of complex missions.

Supports synthesis of independent controllers for sub-missions.

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.