Formal verification of an autonomous personal robotic assistant

M. Webster, C. Dixon, M. Fisher, Maha Salem, Joe Saunders, Kheng Koay, K. Dautenhahn

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

22 Citations (Scopus)
110 Downloads (Pure)


Human–robot teams are likely to be used in a variety of situations wherever humans require the assistance of robotic systems. Obvious examples include healthcare and manufacturing, in which people need the assistance
of machines to perform key tasks. It is essential 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 ™ . We describe how a model of Care-O-bot and its environment was developed using Brahms, a multiagent
workflow language. Formal verification was then carried out by translating this to the input language of an existing model checker. Finally we present some formal
verification results and describe how these could be complemented by simulation-based testing and realworld end-user validation in order to increase the practical and perceived safety and trustworthiness of robotic
Original languageEnglish
Title of host publicationFormal Verification and Modeling in Human-Machine Systems
Subtitle of host publicationPapers from the AAAI Spring Symposium (FVHMS 2014)
ISBN (Print)978-1-57735-655-4
Publication statusPublished - Mar 2014


Dive into the research topics of 'Formal verification of an autonomous personal robotic assistant'. Together they form a unique fingerprint.

Cite this