Tech Reports

ULCS-17-003

Verification for a Robotic Assistant

Paul Gainer

Abstract

The Care-O-Bot is an autonomous robotic assistant that is designed to provide companionship for a person living in a typical domestic environment. Currently the industrial development of the Care-O-Bot, and other robotic assistants, is inhibited by the absence of a coherent framework that can ensure their safety. The EPSRC funded project Trustworthy Robotic Assistants (TRA) aims to develop robots so that they can engage in advanced interactions with humans in a safe and trustworthy manner; this incorporates the development of new tools and techniques to verify and validate robotic assistants.

The functionality of the Care-O-Bot is determined by a set of control rules which are grouped together to form behaviours, high level rules which determine how the robot acts in its environment. This project is based on work undertaken as part of the TRA project in which model checking techniques were applied to verify a set of Care-O-Bot behaviours.

In previous work models of the robot behaviours, and its environment, were constructed by hand and used as input for the model checkers NuSMVand Spin, software tools that automate the model checking process. This report details the design, realisation and evaluation of an automatic translation from sets of Care-O-Bot control rules into input for the model checker NuSMV.

Initially an extensive analysis of a set of Care-O-Bot control rules is conducted. The results of this analysis are used to design an initial translation from control rules into a succinct intermediate form representation, then a second translation from this intermediate form into NuSMV input. The realisation of the design is discussed and the resulting software is tested and shown to be an effective solution to the problem. Finally, conclusions are drawn that determine a measure of success for the project.

For each technical report listed here, copyright and all intellectual property rights remain with the respective authors. Copyright is effective from the year of publication in each case. By downloading a file from this page, you agree to use it only for purposes of research and scholarship. Any other use of this material or storage of it in any medium or its sale or distribution in any form is expressly forbidden without prior written permission from the authors concerned.