Formal Specification and Verification of the Safe Interaction between Humans and Industrial Robots

The studentship, which has a start date of 8^th February 2021, will focus on expressing and formally verifying properties concerning the safety of humans interacting with industrial robots used in advanced manufacturing. There is a lot of flexibility concerning the actual technical work to be pursued, which will be determined together with the student by taking into consideration their skills and preferences. In this area, we are looking into a vast possible space of pioneering research under the direction of highly motivated supervisors located at Sheffield's Computer Science department and Advanced Manufacturing Research Centre (AMRC).

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.

Remote Start

Due to the ongoing Covid-19 pandemic and each candidate's personal circumstances, there may be the opportunity to start the PhD remotely, with the view to arriving in Sheffield when appropriate. This will be discussed with each candidate on an individual basis.

About the University

The PhD will be pursued in the Department of Computer Science, part of the Faculty of Engineering at the University of Sheffield. The PhD student will benefit from a research-intensive environment, spanning the Security of Advanced Systems Verification and Testing groups (https://www.sheffield.ac.uk/dcs/research/groups), of Sheffield Robotics (https://www.sheffield.ac.uk/sheffieldrobotics) and the AMRC (https://www.amrc.co.uk/). The University of Sheffield is a member of the Russell Group, and is consistently ranked among the world’s top 100 universities. In 2019, it was named number one in the UK for engineering research income and investment (https://www.sheffield.ac.uk/news/nr/engineering-research-number-one-universities-uk-best-study-collaborate-1.845379). At the most recent Research Excellence Framework (REF 2014) evaluation, the Sheffield Department of Computer Science was ranked 5th in the UK according to research output quality. 

For further information about the studentship, please contact Dr Andrei Popescu directly via [Email Address Removed]

Required Qualifications

Candidates should have at least a 2:1 BSc degree in Computer Science or a closely related subject.

Desirable skills:

Excellent programming skills

Solid grasp of logic and mathematics

Familiarity with verification tools such as theorem provers and model checkers

Motivation for pursuing high-quality research and publishing it in top-tier conferences and journals

If English is not the applicant’s first language, they must have an IELTS score of 6.5 overall, with no less than 6.0 in each component. 

How to apply

Please apply directly to the University of Sheffield using the online application system

Complete an application for admission to the standard Computer Science PhD programme, naming Dr Andrei Popescu as proposed supervisor.

Applications should include research proposal, CV, degree certificate, transcripts and two academic references.