P. Gainer, C. Dixon, K. Dautenhahn, M. Fisher, U. Hustadt, J. Saunders and M. Webster (2017): ``CRutoN: Automatic Verification of a Robotic Assistant's Behaviour.'' In L. Petrucci, C. Seceleanu and A. Cavalcanti, editors, Proceedings of the Joint 22nd International Workshop on Formal Methods for Industrial Critical Systems and 17th International Workshop on Automated Verification of Critical Systems (FMICS-AVoCS 2017) [Turin, Italy, 18-20 September 2017], pp. 119-133. LNCS 10471, Springer, 2017.
Abstract, BibTeX, PDF (© Springer).

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.


Maintained by Ullrich Hustadt, U.Hustadt@liverppol.ac.uk, last updated Monday, 02-Apr-2018 21:09:40 BST © 2018 by Ullrich Hustadt.