Effectively specifying and implementing robotic missions pose a set of challenges to software engineering for robotic systems, since they require formalizing and executing 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 a tedious and error-prone task. Moreover, as the number of context, hence the specification, becomes more complex, 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 sub-missions, with each sub-mission corresponding to a specific context. However, such a compositional approach would still pose challenges in ensuring the overall mission correctness. In this paper, we propose a new, compositional framework for the specification and implementation of contextual robotic missions using assume-guarantee contracts. The mission specification is captured in a hierarchical and modular way and each sub-mission is synthesized as a robot controller. We address the problem of dynamically switching between sub-mission controllers while ensuring correctness under certain conditions.

翻译：有效规约与实现机器人任务给机器人系统的软件工程带来了一系列挑战，因为这需要在现实运行环境中考虑各种应用场景和条件（即上下文）的同时，形式化并执行机器人的高层任务。编写能显式考虑多重上下文的正确任务规约是一项繁琐且易错的工作。此外，随着上下文数量（进而规约复杂度）的增加，通过合成方法生成正确性构造的实现将变得难以处理。解决这些问题的可行方法是将任务规约分解为更小的子任务，每个子任务对应一个特定上下文。然而，这种组合方法在确保整体任务正确性时仍会面临挑战。本文提出一种新的组合框架，利用假设-保证合约实现上下文机器人任务的规约与实现。任务规约以分层模块化方式捕获，每个子任务被合成为机器人控制器。我们解决了在特定条件下确保正确性的同时，动态切换子任务控制器的问题。