CRutoN: Automatic Verification of a Robotic Assistant's Behaviours

Gainer, P, Dixon, CL, Dautenhahn, K, Fisher, M, Hustadt, U, Saunders, J and Webster, M (2017) CRutoN: Automatic Verification of a Robotic Assistant's Behaviours. In: FMICS/AVOCS 2017, 2017-9-18 - 2017-9-20, Torino, Italy.

Text paper_28.pdf - Author Accepted Manuscript Download (1MB)

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.

Item Type:	Conference or Workshop Item (Unspecified)
Uncontrolled Keywords:	4613 Theory Of Computation, 46 Information and Computing Sciences, 4602 Artificial Intelligence
Depositing User:	Symplectic Admin
Date Deposited:	06 Jul 2017 13:10
Last Modified:	20 Jun 2024 19:09
DOI:	10.1007/978-3-319-67113-0_8
Related URLs:	Author Publisher
URI:	https://livrepository.liverpool.ac.uk/id/eprint/3008342