基于契约的上下文机器人任务正确构造设计
软件工程
2024-01-02 v3 机器人学
摘要
有效规约与实现机器人任务对机器人系统的软件工程提出了一系列挑战。这些挑战源于需要形式化并执行机器人的高层任务，同时考虑真实操作环境中的各种应用场景与条件（亦称上下文）。编写显式考虑多个上下文的正确任务规约可能繁琐且易错。此外，随着上下文数量及相应规约复杂度的增加，生成正确构造的实现（例如通过使用综合方法）可能变得难以处理。解决这些问题的一种可行方法是将任务规约分解为更小、可管理的子任务，每个子任务针对特定上下文定制。然而，这种组合方法在确保整体任务正确性方面引入了其自身的挑战。在本文中，我们提出一种使用假设-保证契约来规约与实现上下文机器人任务的新颖组合框架。任务规约以层次化与模块化方式构建，允许每个子任务被综合为独立的机器人控制器。我们解决了在预定义条件下动态切换子任务控制器同时确保正确性的问题。
引用
@article{arxiv.2306.08144,
title = {Correct-by-Construction Design of Contextual Robotic Missions Using Contracts},
author = {Piergiuseppe Mallozzi and Pierluigi Nuzzo and Nir Piterman and Gerardo Schneider and Patrizio Pelliccione},
journal= {arXiv preprint arXiv:2306.08144},
year = {2024}
}