Towards language-based verification of robot behaviors
Towards language-based verification of robot behaviors
复制标题
迈向基于语言的机器人行为验证
DOI：
10.1109/iros.2011.6095028
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
C. J. Taylor
中科院分区：
文献类型：
--
作者：
Anthony Cowley;C. J. Taylor
有限资源的管理是许多机器人行为的核心。一些机器人系统必须保持关于平衡的脚的布置的不变量，另一些机器人系统具有用于操纵其环境的抓持器，而另一些机器人系统必须遵守管理环境中的对象的使用的严格规则。然而，这种资源管理职责的细节几乎普遍被锁定在不透明的控制器后面，这些控制器缺乏类型信息，这极大地阻碍了严格的静态分析。我们提出了一个应用程序的依赖类型理论和线性逻辑的机器人行为程序，管理机器人和环境状态的静态分析，与工作的装配任务的例子。这种方法提供了静态的，正式的保证，相对于附加到原始动作的安全要求，以及在脚本化的动作序列的每个步骤的预期状态的自省，允许自动生成的动态的，基于传感器的，运行时验证的成功执行。
The management of finite resources is central to many robot behaviors. Some robotic systems must maintain invariants regarding the disposition of feet for balancing, others have grippers for manipulating their environments, while yet others must respect strict rules governing the usage of objects in the environment. Yet the specifics of such resource management responsibilities are almost universally locked behind opaque controllers whose lack of type information greatly impedes rigorous static analysis. We present an application of dependent type theory and linear logic for the static analysis of robot behavior programs that manage both robot and environment state, with a worked assembly task example. This approach offers static, formal guarantees with respect to safety requirements attached to primitive actions, as well as introspection of expected state at each step of a scripted sequence of actions allowing for the automatic generation of dynamic, sensor-based, runtime verification of successful execution.