@inproceedings{9d425027496349d588a526d4468caf60,
title = "CRutoN: Automatic Verification of a Robotic Assistant{\textquoteright}s Behaviours",
abstract = "The Care-O-bot is an autonomous robotic assistant that can support people in domestic and other environments. The behaviour of the robot can be defined by a set of high level control rules. The adoption and further development of such robotic assistants is inhibited by the absence of assurances about their safety. In previous work, formal models of the robot behaviour and its environment were constructed by hand and model checkers were then used to check whether desirable formal temporal properties were satisfied for all possible system behaviours. In this paper we describe the details of the software CRutoN, that provides an automatic translation from sets of robot control rules into input for the model checker NuSMV. We compare our work with previous attempts to formally verify the robot control rules, discuss the potential applications of the approach, and consider future directions of research.",
author = "Paul Gainer and Clare Dixon and Kerstin Dautenhahn and Michael Fisher and Ullrich Hustadt and Joe Saunders and Matt Webster",
year = "2017",
doi = "10.1007/978-3-319-67113-0_8",
language = "English",
isbn = "9783319671123",
volume = "10471 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "119--133",
booktitle = "Critical Systems: Formal Methods and Automated Verification - Joint 22nd International Workshop on Formal Methods for Industrial Critical Systems and 17th International Workshop on Automated Verification of Critical Systems, FMICS-AVoCS 2017, Proceedings",
address = "Germany",
note = "22nd International Workshop on Formal Methods for Industrial Critical Systems and 17th International Workshop on Automated Verification of Critical Systems, FMICS-AVoCS 2017 ; Conference date: 18-09-2017 Through 20-09-2017",
}