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 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
assistants.
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
assistants.
| Original language | English |
|---|---|
| Title of host publication | Formal Verification and Modeling in Human-Machine Systems |
| Subtitle of host publication | Papers from the AAAI Spring Symposium (FVHMS 2014) |
| Publisher | AAAI |
| Pages | 74-79 |
| ISBN (Print) | 978-1-57735-655-4 |
| Publication status | Published - Mar 2014 |