Trustworthy Robotic Assistants

Lead Research Organisation: University of the West of England
Department Name: Faculty of Environment and Technology

Abstract

Abstracts are not currently available in GtR for all funded research. This is normally because the abstract was not required at the time of proposal submission, but may be because it included sensitive information such as personal details.

Publications

10 25 50
 
Description Reliability and Safety. We conducted formal verification of an autonomous personal care robot, Care-o-bot, deployed within the University of Hertfordshire's Robot House test facility. We modelled the Care-o-bot's behaviour formally using Brahms, a high-level agent programming language. Using a software tool developed in-house, they were able to translate Brahms into Promela, the input language to the model checker Spin. Safety- and mission-critical requirements were translated into formal properties expressed in LTL and were then formally verified using Spin. This provided a higher level of confidence in the abiity of Care-o-bot to take care of a person in the Robot House. In subsequent work an expanded set of properties was used to formalise a wider range of requirements, further increasing the confidence in Care-o-bot and further demonstrating the effectiveness of formal verification for human-robot interaction scenarios.

We demonstrated the benefits of using coverage-driven verification to automate a large part of simulation-based testing of code used to control robots that directly interact with humans on the example of a human-robot collaborative manufacturing task. We then focused on the problem of efficiently generating effective tests. We developed a very effective model-based approach that made use of the models developed for formal verification and model checking in the test generation process. This approach is capable of directing test generation to hard to reach and critical interaction scenarios. To further increase the level of automation, we then introduced agency into the verification environment by modeling the human and the environment the robot interacts with as agents. Our most recent results show that using multi-agent systems as models for test generation is as effective as the more traditional method of model checking automata, with the extra benefits of multi-agent models being small, in the number of lines of code when compared to the automata, and model traversal time being low and constant.

Ethics and Trust. We explored the viability of verifying formally whether an autonomous system is capable of behaving ethically. There are many different ethical systems across different societies, and it may be useful for definitions of ethical behaviour to change. A high-level agent programming language, Ethan, was devised to allow autonomous agents to be programmed with additional ethical requirements. Then, an existing agent interpreter and model checker were extended to allow for the formal verification of ethical behaviour. Human-robot interaction studies into trust and trustworthiness gave important insights into how people perceive robots performing different types of tasks with different levels of robot performance and communication abilities.

Verifying Robotic Systems. We have also made progress towards the holistic framework for the V&V of autonomous robotic assistants, as depicted in the earlier diagram. As part of the programme of populating the holistic framework, we have carried out testing of algorithms in and formal verification of autonomy.
Exploitation Route Techniques for verification of human-robot interaction used in subsequent research proposals and beginning to have an impact on robotics industry and regulatory/standards context.
Sectors Agriculture, Food and Drink,Healthcare,Manufacturing, including Industrial Biotechology,Transport

URL http://robosafe.csc.liv.ac.uk/
 
Description Led on to subsequent EPSRC proposals and Innovate UK projects in the Connected Autonomous Vehicle sector Work in this project has helped inform BSI Robot Safety and Robot Ethics standards. Testing techniques developed are being taken up by industry. Findings led to several new PhD student projects that will further illuminate issues of safety, reliability, trust, and trustworthiness for robots operating in human-inhabited environments. New collaborations with industry through three CASE studentships have been initiated
First Year Of Impact 2014
Sector Healthcare,Manufacturing, including Industrial Biotechology,Transport
Impact Types Societal

 
Description CAPRI: Connected and Autonomous Vehicles 2 (CCAV) - Stream 2
Amount £356,198 (GBP)
Funding ID 103288 
Organisation Innovate UK 
Sector Public
Country United Kingdom
Start 10/2017 
End 03/2020
 
Description CAV Forth
Amount £4,350,959 (GBP)
Funding ID 190423 
Organisation Innovate UK 
Sector Public
Country United Kingdom
Start 04/2019 
End 09/2021
 
Description ROBOPILOT
Amount £6,820,883 (GBP)
Funding ID 103703 
Organisation Innovate UK 
Sector Public
Country United Kingdom
Start 01/2018 
End 12/2019
 
Description Project academic partner institutions 
Organisation University of Bristol
Department School of Geographical Sciences
Country United Kingdom 
Sector Academic/University 
PI Contribution This project was a collaborative one with the Universities of Liverpoll, Bristol and Hertfordshire
Collaborator Contribution We worked togethe rin close collbaoraiotn throughout the project
Impact Several publications as listed
Start Year 2013
 
Description Project academic partner institutions 
Organisation University of Hertfordshire
Department Centre for Research in Primary and Community Care (CRIPACC)
Country United Kingdom 
Sector Academic/University 
PI Contribution This project was a collaborative one with the Universities of Liverpoll, Bristol and Hertfordshire
Collaborator Contribution We worked togethe rin close collbaoraiotn throughout the project
Impact Several publications as listed
Start Year 2013
 
Description Project academic partner institutions 
Organisation University of Liverpool
Department Department of Chemistry
Country United Kingdom 
Sector Academic/University 
PI Contribution This project was a collaborative one with the Universities of Liverpoll, Bristol and Hertfordshire
Collaborator Contribution We worked togethe rin close collbaoraiotn throughout the project
Impact Several publications as listed
Start Year 2013