"The Fridge Door is Open"-Temporal Verification of a Robotic Assistant's Behaviours
"The Fridge Door is Open"-Temporal Verification of a Robotic Assistant's Behaviours
复制标题
“冰箱门是开着的”——机器人助手行为的时间验证
DOI：
10.1007/978-3-319-10401-0_9
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
K. Dautenhahn
中科院分区：
文献类型：
--
作者：
C. Dixon;M. Webster;J. Saunders;Michael Fisher;K. Dautenhahn
机器人助手被设计为在各种情况下帮助或与人类一起工作，从家庭情况下的援助，通过医疗保健，到工业环境。虽然机器人已经在工业中使用了一段时间，但它们通常在运动范围或任务范围方面受到限制。新一代的机器人助手有更多的行动自由，能够自主做出决定，并在各种选择之间做出决定。要让人们采用这样的机器人，他们必须被证明是安全和值得信赖的。在本文中，我们专注于正式验证的一组规则，已开发控制护理O-机器人，位于一个典型的国内环境中的机器人助手。特别是，我们应用模型检查，一个自动化和详尽的算法技术，检查是否正式的时间属性满足所有可能的行为的系统。我们证明了一些与机器人行为相关的属性，它们的优先级和可中断性，有助于支持机器人行为的安全性和可信度。
Robotic assistants are being designed to help, or work with, humans in a variety of situations from assistance within domestic situations, through medical care, to industrial settings. Whilst robots have been used in industry for some time they are often limited in terms of their range of movement or range of tasks. A new generation of robotic assistants have more freedom to move, and are able to autonomously make decisions and decide between alternatives. For people to adopt such robots they will have to be shown to be both safe and trustworthy. In this paper we focus on formal verification of a set of rules that have been developed to control the Care-O-bot, a robotic assistant located in a typical domestic environment. In particular, we apply model-checking, an automated and exhaustive algorithmic technique, to check whether formal temporal properties are satisfied on all the possible behaviours of the system. We prove a number of properties relating to robot behaviours, their priority and interruptibility, helping to support both safety and trustworthiness of robot behaviours.
DOI：
--
发表时间：
2014
期刊：
--
影响因子：
--
作者：
Webster M
通讯作者：
Webster M