Formal Verification of Human-Agent-Robot Teamwork using Brahms

Speaker: Dr Richard Stocker, Senior Lecturer, Computer Science, University of Chester
Venue: University of Chester, Thornton Science Park, Room TSU106
Date: 10/1/2018 10:00 - 11:00


The world of robotics is still in its infancy, the robots we have now are excellent at automating a simple deterministic task but struggle when we bring them into a non-deterministic environment. The potential application of robotics is massive, ranging from dangerous but life-saving jobs (such as search and rescue) to simple everyday tasks such as vacuuming the floor.  When we are dealing with a scenario involving the interaction of humans and robots we often deem this as `safety-critical’, since the robot may harm the human.  In these safety-critical scenarios it is preferential to simulate the interactions of the human and the robot, based on the robots programmed protocols, to identify whether anything dangerous could occur or if the task will fail.  One such tool for this is Brahms, a human-agent-robot simulation tool developed at NASA to model scenarios such as exploring the Victoria crater on Mars, backing up data from the International Space Station, and modelling the Überlingen mid-air collision.  One of the limitations of Brahms was that it was only capable of displaying a single simulation at a time, so in order to evaluate the safety/effectiveness of a scenario they would have to run the simulation multiple times and manually determine the possibility of failure.  To combat this we developed verification tools for Brahms which will run every possible simulation (based on specific points of non-determinism), each simulation is automatically checked against specifications in order to determine if it results in something undesirable happening.  In this talk we will discuss Brahms, its applications, the verification of Brahms programs, and how we have extended Brahms to measure the workload of the humans in a simulation.

Speaker's Bio

Dr Richard Stocker holds a PhD in the Verification of Human Agent Teamwork from the University of Liverpool in 2013. He worked as a post-doctoral research associate at NASA Ames in California for two years (2013-2015).  There he developed tools for the verification and validation of human agent interactions working with many researchers and helping interns with their projects.  After this position ended he became an associate lecturer at Middlesex University until 2017, teaching on the foundation year.  Richard then joined the University of Chester in November of 2017 as a senior lecturer.

Richard’s research interests lie in the verification and validation of human-agent simulations; to develop tools and techniques for modelling and simulating humans and agents, and verify their interactions.  The tool he created during his PhD looked at scenarios involving robots in healthcare; modelling robots working with doctors and nurses to treat patients.  His work at NASA extended his PhD, creating a new and improved version of his tool which would then be used to model airline pilots and their interaction with the aeroplane and air traffic controllers.  This extension included the ability to model workload, meaning he could model different scenarios and determine which involved the highest workloads for the human participants.

Leave a Reply