一种可验证且构造即正确的机器人功能层级控制器
机器人学
2013-09-03 v1 软件工程
摘要
自主机器人是复杂的系统，需要众多异构软件组件之间的交互与协作。近年来，机器人越来越多地用于复杂且安全关键的任务，例如火星探测以及辅助或替代人类。因此，机器人已成为必须满足安全属性的关键系统，特别是逻辑、时间和实时约束。为此，我们提出了面向自主系统的 LAAS 架构（尤其是其 GenoM 工具）的演进版本。该演进依赖于基于组件的 BIP 设计框架，该框架已成功应用于嵌入式系统等其他领域。我们展示了如何将 BIP 集成到现有的机器人最低（功能）层级开发方法中。具体而言，我们讨论了功能层级的组件化、其执行控制器的综合，以及如何验证所得到的功能层级是否符合无死锁等属性。我们还通过实验表明，该验证对于复杂的现实世界机器人系统是可行且可用的；尽管存在执行开销，但基于我们新方法生成的基于 BIP 的功能层级在实际机器人平台上仍然具有实用性。我们的方法已在 LAAS 架构中完全实现，并在真实机器人上进行了多次实验。
引用
@article{arxiv.1309.0442,
title = {A Verifiable and Correct-by-Construction Controller for Robot Functional Levels},
author = {Saddek Bensalem and Lavindra de Silva and Félix Ingrand and Rongjie Yan},
journal= {arXiv preprint arXiv:1309.0442},
year = {2013}
}