Trustworthy Robotic Assistants
Lead Research Organisation:
University of Bristol
Department Name: Computer Science
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.
People |
ORCID iD |
| Kerstin Eder (Principal Investigator) |
Publications
Amirabdollahian F
(2013)
Can you trust your robotic assistant?
Araiza-Illan D
(2016)
Towards Autonomous Robotic Systems
Araiza-Illan D
(2019)
Humanoid Robotics: A Reference
Araiza-Illan D
(2015)
Hardware and Software: Verification and Testing
| 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 ability 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 high-level formal models and properties developed for formal verification and employed model checking in the test generation process. This approach is capable of directing test generation to hard to reach and critical interaction scenarios. By combining formal verification with simulation and test-based verification approaches we can benefit from their advantages and overcome their limitations, gaining a more comprehensive verification result overall. 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 and validation of human-robot interaction are the subject of subsequent research proposals and are beginning to have an impact on the robotics industry and regulatory/standards context. End users and tool providers have expressed an interest in using the techniques we have developed for the verification of autonomous systems. In particular, the model-based test generation techniques are being further developed in the context of two Innovate UK CAV-2 awards in collaboration with industry. |
| Sectors | Digital/Communication/Information Technologies (including Software),Healthcare,Manufacturing, including Industrial Biotechology,Transport |
| URL | http://robosafe.csc.liv.ac.uk/ |
| Description | Connected and Autonomous Vehicles 2 (CAV-2) CAPRI |
| Amount | £4,200,000 (GBP) |
| Funding ID | 103288 |
| Organisation | Innovate UK |
| Sector | Public |
| Country | United Kingdom |
| Start | 10/2017 |
| End | 09/2020 |
| Description | Connected and Autonomous Vehicles 2 (CAV-2) ROBOPILOT |
| Amount | £6,820,000 (GBP) |
| Funding ID | 103703 |
| Organisation | Innovate UK |
| Sector | Public |
| Country | United Kingdom |
| Start | 01/2018 |
| End | 03/2021 |
| Description | EPSRC iCASE award with Thales on Testing Agents for Verification of Autonomous Systems |
| Amount | £30,000 (GBP) |
| Funding ID | 18000191 |
| Organisation | Thales Group |
| Department | Thales UK Limited |
| Sector | Private |
| Country | United Kingdom |
| Start | 10/2018 |
| End | 09/2022 |
| Description | Industrial CASE Award |
| Amount | £27,150 (GBP) |
| Funding ID | 16000135 voucher code |
| Organisation | Engineering and Physical Sciences Research Council (EPSRC) |
| Sector | Public |
| Country | United Kingdom |
| Start | 09/2017 |
| End | 08/2021 |
| Description | Innovate UK Software Verification and Validation for Complex Systems |
| Amount | £8,101 (GBP) |
| Funding ID | 66584-471175 |
| Organisation | Innovate UK |
| Sector | Public |
| Country | United Kingdom |
| Start | 05/2016 |
| End | 04/2017 |
| Description | Innovate UK Software Verification and Validation for Complex Systems |
| Amount | £6,511 (GBP) |
| Funding ID | 65045-471140 |
| Organisation | Innovate UK |
| Sector | Public |
| Country | United Kingdom |
| Start | 05/2016 |
| End | 04/2017 |
| Description | Two CASE studentships in collaboration with Infineon |
| Amount | £70,000 (GBP) |
| Organisation | Engineering and Physical Sciences Research Council (EPSRC) |
| Sector | Public |
| Country | United Kingdom |
| Start | 10/2017 |
| End | 09/2021 |
| Description | UKRI Trustworthy Autonomous Systems Node in Functionality |
| Amount | £3,315,003 (GBP) |
| Funding ID | EP/V026518/1 |
| Organisation | Engineering and Physical Sciences Research Council (EPSRC) |
| Sector | Public |
| Country | United Kingdom |
| Start | 11/2020 |
| End | 04/2024 |
| Title | A Corroborative Approach to Verification and Validation of Human-Robot Teams: Data from Simulations and Experiments |
| Description | This dataset contains recordings and results from simulations and experiments of a robot to human object handover task that served as case study in the paper "A Corroborative Approach to Verification and Validation of Human-Robot Teams," by Matt Webster, David Western, Dejanira Araiza-Illan, Clare Dixon, Kerstin Eder, Michael Fisher and Anthony G. Pipe. Preferred dataset citation: David Western, Dejanira Araiza-Illan, Anthony G. Pipe and Kerstin Eder (2019): A Corroborative Approach to Verification and Validation of Human-Robot Teams: Data from Simulations and Experiments. University of Bristol Research Data Repository. |
| Type Of Material | Database/Collection of data |
| Year Produced | 2019 |
| Provided To Others? | Yes |
| Impact | This dataset provided the evidence for the associated research paper published in The International Journal of Robotics Research. |
| URL | https://data.bris.ac.uk/data/dataset/gw4qbvkmmekl1rlkgaqskdtyd |
| Title | BiB - Believing in BERT |
| Description | The BiB study investigated the benefits of an affective physical interaction with a humanoid robot by comparing an expressive and communicative condition with a faster, less error prone but non-communicative one. The BiB study was conducted as part of the Trustworthy Robotic Assistants (ROBOSAFE) project. Preferred data citation: Adriana Hamacher, Nadia Bianchi-Berthouze, Anthony G. Pipe and Kerstin Eder (2016): BiB - Believing in BERT. |
| Type Of Material | Database/Collection of data |
| Year Produced | 2016 |
| Provided To Others? | Yes |
| Impact | This dataset provides the evidence for the related paper "Believing in BERT: Using expressive communication to enhance trust and counteract operational error in physical Human-robot interaction" published at IEEE RO-MAN. |
| URL | https://data.bris.ac.uk/data/dataset/1xkj9m7z4vi6l137gihezyd9o3 |
| Description | Autonomous Systems Verification and Validation collaboration with Thales UK |
| Organisation | Thales Group |
| Department | Thales UK Limited |
| Country | United Kingdom |
| Sector | Private |
| PI Contribution | Expertise in test-based verification and validation for autonomous intelligent systems as developed in the RIVERAS/ROBOSAFE projects. |
| Collaborator Contribution | Thales provides industrial expertise and use cases from their Autonomous Systems range for us to work on. |
| Impact | joint applications for further funding (iCASE award and also Dstl application) |
| Start Year | 2017 |
| Description | Dagstuhl Seminar 19081: Verification and Synthesis of Human-Robot Interaction |
| Organisation | Cornell University |
| Country | United States |
| Sector | Academic/University |
| PI Contribution | I co-organized this Dagstuhl Seminar with colleagues from LAAS, France, and Cornell University, US. The seminar brought together experts in computational HRI, verification and synthesis of autonomous systems, formal methods, simulation-based testing, and cognitive and social psychology to exchange ideas, define research directions, and foster collaborations toward a new theory and practice of verifiable HRI. In particular, I contributed expertise in formal and test-based verification techniques for robots that work in close/direct collaboration with humans. |
| Collaborator Contribution | I co-organized this Dagstuhl seminar with Rachid Alami (LAAS - Toulouse, FR), Guy Hoffman (Cornell University - Ithaca, US) and Hadas Kress-Gazit (Cornell University - Ithaca, US). They cover AI and robotics, synthesis and human-human/robot interaction. The seminar had more than 40 participants from a variety of backgrounds covering Human-Robot Interaction, Verification, Synthesis, Formal Methods and Testing and working in academia, industry or commercial research labs. |
| Impact | 02/2017: Funding application for seminar has been successful. Further outputs are expected after the seminar. 02/2019: This seminar has just taken place (Feb 2019) and we are now preparing the following outputs (full details to follow once published and available): a jointly authored position paper, a literature survey on Verification and Synthesis Techniques for Human-Robot Interaction, and the Dagstuhl Seminar report. This is a multi-disciplinary collaboration, bringing together the verification, validation and synthesis community with the human-human/robot interaction community and the autonomous systems community in general. 12/2019: We submitted a position paper entitled "Formalizing and Guaranteeing* Human-Robot Interaction" to the ACM Magazine Communications of the ACM. This article is still under review at the time of this submission. |
| Start Year | 2017 |
| Description | Dagstuhl Seminar 19081: Verification and Synthesis of Human-Robot Interaction |
| Organisation | University of Toulouse |
| Department | Laboratory for Analysis and Architecture of Systems |
| Country | France |
| Sector | Academic/University |
| PI Contribution | I co-organized this Dagstuhl Seminar with colleagues from LAAS, France, and Cornell University, US. The seminar brought together experts in computational HRI, verification and synthesis of autonomous systems, formal methods, simulation-based testing, and cognitive and social psychology to exchange ideas, define research directions, and foster collaborations toward a new theory and practice of verifiable HRI. In particular, I contributed expertise in formal and test-based verification techniques for robots that work in close/direct collaboration with humans. |
| Collaborator Contribution | I co-organized this Dagstuhl seminar with Rachid Alami (LAAS - Toulouse, FR), Guy Hoffman (Cornell University - Ithaca, US) and Hadas Kress-Gazit (Cornell University - Ithaca, US). They cover AI and robotics, synthesis and human-human/robot interaction. The seminar had more than 40 participants from a variety of backgrounds covering Human-Robot Interaction, Verification, Synthesis, Formal Methods and Testing and working in academia, industry or commercial research labs. |
| Impact | 02/2017: Funding application for seminar has been successful. Further outputs are expected after the seminar. 02/2019: This seminar has just taken place (Feb 2019) and we are now preparing the following outputs (full details to follow once published and available): a jointly authored position paper, a literature survey on Verification and Synthesis Techniques for Human-Robot Interaction, and the Dagstuhl Seminar report. This is a multi-disciplinary collaboration, bringing together the verification, validation and synthesis community with the human-human/robot interaction community and the autonomous systems community in general. 12/2019: We submitted a position paper entitled "Formalizing and Guaranteeing* Human-Robot Interaction" to the ACM Magazine Communications of the ACM. This article is still under review at the time of this submission. |
| Start Year | 2017 |
| Description | Dagstuhl Seminar 19171: Ethics and Trust: Principles, Verification and Validation |
| Organisation | University of Liverpool |
| Country | United Kingdom |
| Sector | Academic/University |
| PI Contribution | I was invited to this seminar based on my expertise in verification and validation for safety in robots and autonomous systems. I contributed a presentation and worked in two different working groups. We are in the process of writing a joint paper. |
| Collaborator Contribution | They organised this Dagstuhl Seminar. |
| Impact | none yet |
| Start Year | 2019 |
| Description | Dagstuhl Seminar 19171: Ethics and Trust: Principles, Verification and Validation |
| Organisation | University of Liverpool |
| Country | United Kingdom |
| Sector | Academic/University |
| PI Contribution | I was invited to this seminar based on my expertise in verification and validation for safety in robots and autonomous systems. I contributed a presentation and worked in two different working groups. We are in the process of writing a joint paper. |
| Collaborator Contribution | They organised this Dagstuhl Seminar. |
| Impact | none yet |
| Start Year | 2019 |
| Description | Network on the Verification and Validation of Autonomous Systems |
| Organisation | University of Liverpool |
| Department | Department of Computer Science |
| Country | United Kingdom |
| Sector | Academic/University |
| PI Contribution | Presentations on the state of the art of test-based verification techniques, participation and contribution to networking events, organisation of a workshop. |
| Collaborator Contribution | Leading network activities, organising networking events, community building, dissemination, research roadmap shaping, etc |
| Impact | community building to date |
| Start Year | 2015 |
| Description | Agent Verification Workshop associated with TAROS 2015 |
| Form Of Engagement Activity | Participation in an activity, workshop or similar |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Postgraduate students |
| Results and Impact | A workshop on Agent Verification Techniques to which I contributed a session on "Theorem Proving and Testing for Autonomous Systems" and participated at a panel on "Current Research Challenges in Agent Verification" which sparked interesting questions. A summary of the panel was created and will feed into a research roadmap in the context of the Network on the Verification and Validation of Autonomous Systems. |
| Year(s) Of Engagement Activity | 2015 |
| URL | http://cgi.csc.liv.ac.uk/~maryam/AVWorkshop15.html |
| Description | Article in the Space Safety Magazine |
| Form Of Engagement Activity | A magazine, newsletter or online publication |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Professional Practitioners |
| Results and Impact | article sparked interest in our research into safe Human-Robot Interaction further requests have been made to contribute towards magazine articles and Dr Eder was interviewed by the local radio |
| Year(s) Of Engagement Activity | 2014 |
| URL | http://www.spacesafetymagazine.com/aerospace-engineering/robotics/moving-towards-safety-assurance-au... |
| Description | Dagstuhl Seminar 17071 on Assisted Engineering for Robotics and Autonomous Systems (CAREAS) |
| Form Of Engagement Activity | Participation in an activity, workshop or similar |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Industry/Business |
| Results and Impact | This event was focused on Computer Assisted Engineering for Robotics and Autonomous Systems and addressed both academics as well as industrial developers and researchers. An entire week was devoted to discussions, identification of challenges, knowledge exchange and problem solving. New collaborations have already been established since then, e.g. with industrial collaborators who are sharing my interest in the verification of human assistive robots. |
| Year(s) Of Engagement Activity | 2017 |
| URL | https://www.dagstuhl.de/en/program/calendar/semhp/?semnr=17071 |
| Description | Dynamic Testing Workshop |
| Form Of Engagement Activity | Participation in an activity, workshop or similar |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Industry/Business |
| Results and Impact | The workshop aimed to develop links between communities (including structural testing, simulation-based testing, safety-critical testing and safety case construction, and formal methods) within academia and industry, so that we can join forces in addressing the intellectual challenges that lead to safe and trustworthy autonomous systems. The unifying theme was verification in the broad sense - the process of gaining confidence that a system meets its specification. In practice no single verification technique (or class of techniques) will be adequate on its own. The workshop was focused on how dynamic testing, specifically, can contribute to autonomous system verification. The workshop resulted in several collaborative project ideas being taken forward by participants. |
| Year(s) Of Engagement Activity | 2018 |
| URL | https://vavas.org/pastevents/workshop-dynamic-testing-for-autonomous-systems-1-2-february-2018/ |
| Description | Invitation to contribute to an Expert Panel on The Advancement of Medical Devices: Robots in Healthcare held at the European Parliament in Brussels |
| Form Of Engagement Activity | A formal working group, expert panel or dialogue |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Policymakers/politicians |
| Results and Impact | my presentation sparked questions and stimulated a discussion on safety of robots and the need to design for safety contacts for future collaboration, invitation to serve on conference programme committees, invitation to attend and present at workshops |
| Year(s) Of Engagement Activity | 2013 |
| Description | Invited presentation at the National Microelectronics Institute's event on Accelerating Verification - faster, smarter |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | National |
| Primary Audience | Professional Practitioners |
| Results and Impact | presentation sparked invitations for more detailed discussions, knowledge transfer and collaborations after the talk a company indicated their interest in taking some of the research further |
| Year(s) Of Engagement Activity | 2014 |
| URL | http://www.nmi.org.uk/events/event-details/verif2014 |
| Description | Invited presentation at the meeting of the ISO WG Committee on Robots and Robotic Devices |
| Form Of Engagement Activity | A formal working group, expert panel or dialogue |
| Part Of Official Scheme? | Yes |
| Geographic Reach | International |
| Primary Audience | Professional Practitioners |
| Results and Impact | I received an invitation to review and to contribute towards the development of the standards offers for collaboration from both academic and industrial partners, nationally and internationally |
| Year(s) Of Engagement Activity | 2013 |
| Description | Invited speaker at the 1st Verification and Validation for Autonomy Technical Working Group meeting |
| Form Of Engagement Activity | A formal working group, expert panel or dialogue |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Other academic audiences (collaborators, peers etc.) |
| Results and Impact | My presentation stimulated a discussion on the need to combine a variety of verification and validation techniques in recognition of the fact that in practice no single technique is adequate to cover a whole system. offers for collaboration and to take this forward jointly |
| Year(s) Of Engagement Activity | 2014 |
| Description | Lecturer at Winterschool on Verification of Robotics |
| Form Of Engagement Activity | Participation in an activity, workshop or similar |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Postgraduate students |
| Results and Impact | Winterschool for graduate students (https://www.cs.york.ac.uk/circus/RoboCalc-event/) Contribution of the session entitled "Practical Techniques for Verification and Validation of Robots" Abstract This session is focused on practical techniques for the verification and validation of autonomous systems from specification via design to the code level. Because no single technique is adequate to cover a whole system in practice, a variety of verification techniques, including formal methods, such as model checking and theorem proving, and state-of-the-art simulation-based methods, will be presented from first principles and brought into the context of robotics. How these techniques can be applied will be illustrated using real-world examples. We will start with the verification of control system designs with respect to high-level requirements, such as stability, using an assertion-based approach that combines simulation-based verification with automatic theorem proving. We will then focus on using model-based techniques to enhance test generation in the context of coverage-driven verification applied to code used in robots that directly interact with humans. The session will finish with the proposal to design autonomous systems "for verification"; this requires a paradigm shift towards more systematic design practices. The research presented in this session is based on collaborations within the EPSRC funded projects "Robust Integrated Verification of Autonomous Systems" and "Trustworthy Robotic Assistants". This session will be supplemented with hands-on demonstrations presented by Dejanira Araiza Illan. |
| Year(s) Of Engagement Activity | 2015 |
| URL | https://www.cs.york.ac.uk/circus/RoboCalc-event/courses/practical-techniques-for-verification-and-va... |
| Description | Radio interview on safety of robotic assistants |
| Form Of Engagement Activity | A press release, press conference or response to a media enquiry/interview |
| Part Of Official Scheme? | No |
| Geographic Reach | Regional |
| Primary Audience | Public/other audiences |
| Results and Impact | interview sparked questions and invitations to contribute to a magazine article received further invitations for interviews |
| Year(s) Of Engagement Activity | 2013 |
| Description | Verification and Control of Cyber-physical Systems: Theory and Applications |
| Form Of Engagement Activity | Participation in an activity, workshop or similar |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Postgraduate students |
| Results and Impact | I gave an invited talk on "Intelligent test generation for advanced coverage-driven verification of robotic code" at this workshop. The event highlighted recent advances and developments in verification in the field of cyber-physical systems (CPSs), motivated by emerging applications involving autonomous systems such as automated vehicles and robotic systems. The talks focused on verification and control of complex CPS's, with the aim to facilitate an in depth understanding of the challenges posed by their hybrid dynamics, interconnected and distributed nature, the presence of exogenous and/or endogenous uncertainty affecting their evolution, their safety and operational critical nature, and with a wide coverage of possible solution methodologies. The goal of the workshop was to expose attendees to cutting edge research in the field, with an eye on both theory and applications, and to encourage the development of new results and the investigation of several important issues in the future of complex CPSs design, promoting novel collaborations. To this purpose, outstanding researchers from leading industries and universities worldwide were brought together by the organizers to offer their vistas on the field. |
| Year(s) Of Engagement Activity | 2016 |
| URL | http://cdc2016.ieeecss.org/workshops.php#w06 |
| Description | Verification and Validation of Sensing and Control Models in Autonomous Systems |
| Form Of Engagement Activity | Participation in an activity, workshop or similar |
| Part Of Official Scheme? | No |
| Geographic Reach | National |
| Primary Audience | Postgraduate students |
| Results and Impact | This event was held as part of the EPSRC funded V&V Network. Researchers, certification experts and students met to present the latest results and to exchange knowledge as well as to foster new collaborations. |
| Year(s) Of Engagement Activity | 2017 |
| URL | https://vavas.org/events/verification-and-validation-of-sensing-and-control-models-in-autonomous-sys... |