Safety Controller Synthesis for a Mobile Manufacturing Cobot

Ioannis Stefanakos, Radu Calinescu, James A. Douthwaite, Jonathan Aitken, James Law

Research output: Chapter in Book/Report/Conference proceedingConference contribution


We present a case study in which probabilistic model checking has been used to synthesise the correct-by-construction safety controller for a mobile collaborative robot (\emph{cobot}) deployed in a prototype manufacturing cell alongside a human operator. The case study used an ICONSYS iAM-R mobile cobot responsible for the execution of a complex machining process comprising tasks requiring the use of multiple machines at different locations within the cell. Within this process, the role of the safety controller was to ensure that the cobot carried out its tasks and movements between task locations without harming the human operator responsible for its supervision and for performing additional tasks. The paper describes our generalisable approach to synthesising the mobile cobot safety controller, and its evaluation using a digital twin of our experimental manufacturing cell at the University of Sheffield Advanced Manufacturing Research Centre in the UK.
Original languageEnglish
Title of host publicationSoftware Engineering and Formal Methods 2022
Subtitle of host publicationProceedings
Number of pages17
Publication statusAccepted/In press - 26 Jul 2022
EventSoftware Engineering and Formal Methods - Humboldt University, Berlin, Germany
Duration: 28 Sept 202230 Sept 2022

Publication series

NameLecture Notes in Computer Science


ConferenceSoftware Engineering and Formal Methods
Abbreviated titleSEFM

Bibliographical note

This is an author-produced version of the published paper. Uploaded in accordance with the publisher’s self-archiving policy. Further copying may not be permitted; contact the publisher for details

Cite this