University of Hertfordshire

CRutoN: Automatic Verification of a Robotic Assistant’s Behaviours

Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • Paul Gainer
  • Clare Dixon
  • Kerstin Dautenhahn
  • Michael Fisher
  • Ullrich Hustadt
  • Joe Saunders
  • Matt Webster
View graph of relations
Original languageEnglish
Title of host publicationCritical 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
PublisherSpringer Verlag
Pages119-133
Number of pages15
Volume10471 LNCS
ISBN (Print)9783319671123
DOIs
Publication statusPublished - 2017
Event22nd International Workshop on Formal Methods for Industrial Critical Systems and 17th International Workshop on Automated Verification of Critical Systems, FMICS-AVoCS 2017 - Turin, Italy
Duration: 18 Sep 201720 Sep 2017

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10471 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Conference

Conference22nd International Workshop on Formal Methods for Industrial Critical Systems and 17th International Workshop on Automated Verification of Critical Systems, FMICS-AVoCS 2017
CountryItaly
CityTurin
Period18/09/1720/09/17

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.

ID: 12797919