TY - GEN
T1 - "The fridge door is open"
T2 - 15th Annual Conf, TAROS 2014
AU - Dixon, C.
AU - Webster, M.
AU - Saunders, Joe
AU - Fisher, M.
AU - Dautenhahn, K.
PY - 2014
Y1 - 2014
N2 - 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.
AB - 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.
U2 - 10.1007/978-3-319-10401-0_9
DO - 10.1007/978-3-319-10401-0_9
M3 - Conference contribution
SN - 978-3-319-10400-3
T3 - Lecture Notes in Computer Science (LNAI)
SP - 97
EP - 108
BT - Advances in Autonomous Robotics
A2 - Mistry, M.
PB - Springer Nature
Y2 - 1 September 2014 through 3 September 2014
ER -