Formal Verification of an Autonomous Personal Robotic Assistant

Webster, Matt ORCID: 0000-0002-8817-6881, Salem, Maha, Dixon, Clare ORCID: 0000-0002-4610-9533, Fisher, Michael and Dautenhahn, Kerstin (2014) Formal Verification of an Autonomous Personal Robotic Assistant. In: AIAA Symposium 2014 Workshop on Formal Verification in Human Machine Systems (FVHMS 2014), USA.

This is the latest version of this item.

Text
cob-verification.pdf - Author Accepted Manuscript
Download (255kB)

Official URL: https://www.aaai.org/Library/Symposia/Spring/ss14-...

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 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 CareO-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 assistants.

Item Type:	Conference or Workshop Item (Paper)
Additional Information:	## TULIP Type: Conference Proceedings (contribution) ##
Depositing User:	Symplectic Admin
Date Deposited:	09 Dec 2014 11:05
Last Modified:	16 Dec 2022 04:42
Related URLs:	Publisher
URI:	https://livrepository.liverpool.ac.uk/id/eprint/2003320