TY - GEN
T1 - CRutoN
T2 - 22nd International Workshop on Formal Methods for Industrial Critical Systems and 17th International Workshop on Automated Verification of Critical Systems, FMICS-AVoCS 2017
AU - Gainer, Paul
AU - Dixon, Clare
AU - Dautenhahn, Kerstin
AU - Fisher, Michael
AU - Hustadt, Ullrich
AU - Saunders, Joe
AU - Webster, Matt
PY - 2017
Y1 - 2017
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85029496657&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-67113-0_8
DO - 10.1007/978-3-319-67113-0_8
M3 - Conference contribution
AN - SCOPUS:85029496657
SN - 9783319671123
VL - 10471 LNCS
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 119
EP - 133
BT - 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
PB - Springer Nature Link
Y2 - 18 September 2017 through 20 September 2017
ER -