论文标题
基于合同的规格改进和维修任务计划
Contract-Based Specification Refinement and Repair for Mission Planning
论文作者
论文摘要
我们解决了使用假定保证合同对机器人任务进行建模，完善和修复形式规格的问题。我们展示了如何在各种抽象级别上对任务规范进行建模，并使用预先实施规格的库来实施它们。假设使用库中的组件无法满足规范。在这种情况下，我们计算一个可以使用库中元素生成的规范的最佳近似值代理。之后，我们提出了一种系统的方法来进行1）搜索并完善库无法满足的规范的“缺失部分”或2）维修当前规范，以便现有库可以完善它。我们的搜索和维修任务要求的方法利用合同之间的商，分离，组成和合并操作。
We address the problem of modeling, refining, and repairing formal specifications for robotic missions using assume-guarantee contracts. We show how to model mission specifications at various levels of abstraction and implement them using a library of pre-implemented specifications. Suppose the specification cannot be met using components from the library. In that case, we compute a proxy for the best approximation to the specification that can be generated using elements from the library. Afterward, we propose a systematic way to either 1) search for and refine the `missing part' of the specification that the library cannot meet or 2) repair the current specification such that the existing library can refine it. Our methodology for searching and repairing mission requirements leverages the quotient, separation, composition, and merging operations between contracts.
