TITLE: Verifying Brahms Human-Robot Teamwork Models
SPEAKER: Richard Stocker (University of Liverpool)

ABSTRACT:

Collaboration between robots and humans is an increasingly important
aspect of industrial and scientific settings. In addition, significant effort is
being put into the development of robot helpers for more general use in the workplace,
at home, and in health-care environments. However, before such robots can
be fully utilised, a comprehensive analysis of their safety is necessary. Formal verification
techniques are regularly used to exhaustively assess system behaviour.
Our aim is to apply such techniques to Brahms, a human-agent-robot modelling
language. We show how to translate from Brahms scenarios, using a formal semantics
for Brahms, into the input language of a model checker.We illustrate the
approach by defining, translating, and verifying a domestic robot helper example.