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.

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