Planning
Team members: Dr Radu Calinescu, Dr Mario Gleirscher, University of York
The aim of the Planning work package is the analysis, design, synthesis, and assurance of safety controllers for use in human-robot collaboration (HRC) settings in the manufacturing domain. An HRC setting typically comprises a mobile or stationary robot (the Cobot) collaborating with one or more human operators on shared repetitive tasks (the Process). The goal is to combine the capabilities of humans and machines in order to improve quality and reduce cost. As an example of HRC in manufacturing, Figure 1 depicts the actors (blue), the important geometric features (boxes and arcs), and sensor-tracked safeguarded areas (red) of a manufacturing work cell. This work cell concept is inspired by a real-world setting in an actual industrial manufacturing company.
An automatic safety controller (ASC) is used to improve occupational safety for the tasks performed in this work cell. The controller is responsible for handling critical events (CEs). For example, when an operator enters the work cell without being supposed to, the ASC would (a) recognise this event through the tracking system of the cell, (b) switch the Cobot and other machine elements into a contextually appropriate safety mode, (c) interact with the operator (e.g., to warn them), and, (d) if the CE is mitigated, switch the work cell back to a mode where the obstructed task can be continued. The steps (a) to (d) suggest a decomposition of the system-level safety requirement derived from hazard analysis and risk assessment (HARA) of the HRC setting. The ASC is a critical Deciding element and, as such, a part of the overall Deciding element of the autonomous system architecture used in the HRC setting. A HARA of the HRC setting usually results in a list of safety requirements specifying and driving the design of the controller. The Planning work package, hence, focuses on the design of discrete-event controllers that can perform the steps (a) to (d), with the main assurance evidence delivered by probabilistic model checking. The resulting methodology is meant to be used by verification engineers who want to model an HRC setting (i.e. actors, activities, actions) focusing the controller behaviour and to verify this behaviour against safety requirements.
Further details of the research outputs from this work package are available in two publications [1,2] and an AAIP Body of Knowledge entry [3].
[1] Gleirscher, M. & Calinescu, R.: Safety Controller Synthesis for Collaborative Robots. Engineering of Complex Computer Systems, 25th International Conference, 28 - 31 October 2020, Singapore, 2020. doi:
[2] Gleirscher, M.: Yap: Tool Support for Deriving Safety Controllers from Hazard Analysis and Risk Assessments. Luckuck, M. & Farrell, M. (Eds.) Formal Methods for Autonomous Systems (FMAS), 2nd Workshop, EPTCS, 329, pp. 31-47, 2020. doi:
[3] Gleirscher, M. & Calinescu, R. Verification of "Deciding" Requirements. Hawkins, R. (Ed.), AAIP Body of Knowledge, Sec. 2.2.4.3, 2020. url:
