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.

翻译：有效规约与实现机器人任务给机器人系统的软件工程带来了一系列挑战。这些挑战源于需要在真实运行环境中考虑各种应用场景与条件（即上下文）的同时，形式化并执行机器人的高层任务。编写显式处理多个上下文的正确任务规约既繁琐又易错。此外，随着上下文数量及规约复杂度的增加，生成正确性构建的实现（例如通过综合方法）可能变得难以处理。解决这些问题的可行方法是将任务规约分解为更小、更易管理的子任务，每个子任务针对特定上下文定制。然而，这种组合式方法在确保整个任务正确性方面引入了自身的一系列挑战。本文提出了一种新颖的组合式框架，使用假设-保证合约来规约与实现上下文感知的机器人任务。任务规约以分层模块化方式构建，允许将每个子任务综合为独立的机器人控制器。我们解决了在确保预定义条件下正确性的同时，动态切换子任务控制器的问题。