Formal Verification of an Autonomous Personal Robotic Assistant

Abstract

Human–robot teams are likely to be used in a variety of situations wherever humans require the assistance of robotic systems. Obvious examples include health-care and manufacturing, in which people need the as-sistance of machines to perform key tasks. It is essen-tial for robots working in close proximity to people to be both safe and trustworthy. In this paper we examine formal verification of a high-level planner/scheduler for autonomous personal robotic assistants such as Care-O-bot R©. We describe how a model of Care-O-bot and its environment was developed using Brahms, a multi-agent workflow language. Formal verification was then carried out by translating this to the input language of an existing model checker. Finally we present some for-mal verification results and describe how these could be complemented by simulation-based testing and real-world end-user validation in order to increase the prac-tical and perceived safety and trustworthiness of robotic assistants. 1