Formal Specification and Verification of the Safe Interaction between Humans and Industrial Robots
Lead Research Organisation:
University of Sheffield
Department Name: Computer Science
Abstract
The project aims are:
1. To understand how to formulate human-safety properties in a realistic and useful manner. Concrete case studies developed at AMRC will be available, including research prototypes of digital twins for collaborating robots. Main components of the research will be (1) to identify for these systems, via interaction with AMRC experts, safety concerns in various scenarios, and (2) to distil these concerns into fully formal requirements expressed in a suitable formalism. Besides the requirements inspired by specific systems at AMRC, one could also consider the general-purpose source of requirements coming from international standards such as "Robots and robotic devices: Safety requirements for industrial robots" (ISO 10218) and "Robots and robotic devices: Collaborative robots" (ISO-TS 15066). The formalization of these standards' safety directives will be useful for the AMRC case studies, while also representing a potential standalone contribution to the formal clarity of the standards. Especially for cobots (collaborative robots), these standards are still very much under development, and an early formal perspective could help not only clarify, but also refine and enrich them.
2. To design of a formal verification framework for such safety properties on running systems. Here, in collaboration with the AMRC case study developers, one could explore several options based on the employed software and the available tools: ranging from the instrumentation of the code to dynamically monitor the desired property, to the synthesis and static verification of property specifications from code, to code generation from specifications verified with a proof assistant. Beyond software-level verification, a challenge will be to factor in the behaviour of different devices that contribute to the safety functionality - which include e-stops, light gates and floor scanners. To properly deal with such hybrid systems, one could also explore mixed approaches, in which certain components are verified and others are only tested.
1. To understand how to formulate human-safety properties in a realistic and useful manner. Concrete case studies developed at AMRC will be available, including research prototypes of digital twins for collaborating robots. Main components of the research will be (1) to identify for these systems, via interaction with AMRC experts, safety concerns in various scenarios, and (2) to distil these concerns into fully formal requirements expressed in a suitable formalism. Besides the requirements inspired by specific systems at AMRC, one could also consider the general-purpose source of requirements coming from international standards such as "Robots and robotic devices: Safety requirements for industrial robots" (ISO 10218) and "Robots and robotic devices: Collaborative robots" (ISO-TS 15066). The formalization of these standards' safety directives will be useful for the AMRC case studies, while also representing a potential standalone contribution to the formal clarity of the standards. Especially for cobots (collaborative robots), these standards are still very much under development, and an early formal perspective could help not only clarify, but also refine and enrich them.
2. To design of a formal verification framework for such safety properties on running systems. Here, in collaboration with the AMRC case study developers, one could explore several options based on the employed software and the available tools: ranging from the instrumentation of the code to dynamically monitor the desired property, to the synthesis and static verification of property specifications from code, to code generation from specifications verified with a proof assistant. Beyond software-level verification, a challenge will be to factor in the behaviour of different devices that contribute to the safety functionality - which include e-stops, light gates and floor scanners. To properly deal with such hybrid systems, one could also explore mixed approaches, in which certain components are verified and others are only tested.
Organisations
People |
ORCID iD |
| Andrei Popescu (Primary Supervisor) | |
| Artur Graczyk (Student) |
Studentship Projects
| Project Reference | Relationship | Related To | Start | End | Student Name |
|---|---|---|---|---|---|
| EP/T517835/1 | 01/10/2020 | 30/09/2025 | |||
| 2496876 | Studentship | EP/T517835/1 | 08/02/2021 | 07/08/2024 | Artur Graczyk |