Correct-by-Construction Design of Contextual Robotic Missions Using Contracts
CoRR(2023)
摘要
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.
更多查看译文
关键词
contextual robotic missions,correct-by-construction
AI 理解论文
溯源树
样例
![](https://originalfileserver.aminer.cn/sys/aminer/pubs/mrt_preview.jpeg)
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要