Citation: Ozkan, M.; Demirci, Z.;
Aslan, Ö.; Yazıcı, A. Safety
Verification of Multiple Industrial
Robot Manipulators with Path
Conflicts Using Model Checking.
Machines 2023, 11, 282. https://
doi.org/10.3390/machines11020282
Academic Editor: Huosheng Hu
Received: 4 January 2023
Revised: 26 January 2023
Accepted: 5 February 2023
Published: 13 February 2023
Copyright: © 2023 by the authors.
Licensee MDPI, Basel, Switzerland.
This article is an open access article
distributed under the terms and
conditions of the Creative Commons
Attribution (CC BY) license (https://
creativecommons.org/licenses/by/
4.0/).
Article
Safety Verification of Multiple Industrial Robot Manipulators
with Path Conflicts Using Model Checking
Metin Ozkan
1,
*, Zekeriyya Demirci
1
, Özge Aslan
2
and Ahmet Yazıcı
1
1
Department of Computer Engineering, Eskisehir Osmangazi University, 26480 Eskisehir, Turkey
2
Department of Computer Engineering, Erzincan Binali Yıldırım University, 24002 Erzincan, Turkey
* Correspondence: meozkan@ogu.edu.tr
Abstract:
Software development for robotic systems is traditionally performed based on simulations,
manual code implementation, and testing. However, this software development approach can cause
safety issues in some scenarios, including multiple robots sharing a workspace. When different robots
are executing individual planned tasks, they may collide when not adequately coordinated. Safety
problems related to coordination between robots may not be encountered during testing, depending
on timing, but may occur during the system’s operation. In this case, formal verification methods can
provide a more reliable means to ensure the safety of robotic systems. This paper uses the formal
method of model checking for the safety verification of multiple industrial robot manipulators with
path conflicts. We give comparative results of two model-checking tools applied to a system with
two robot manipulators. Whole workflows, from requirement specification to testing, are presented.
Keywords: industrial robot; formal verification; model checking; model-driven engineering
1. Introduction
Multiple robot manipulators that carry out independent tasks in a shared workspace
need a solution to avoid mutual collisions. The risk of collision is an issue in various
robotic fields, including industrial and service applications. However, robotic system
software, which requires the evaluation of such issues, is traditionally developed by robotic
system experts. Moreover, manual tests are carried out both in the real system and in the
simulation environment. Therefore, the verification and validation (V&V) of the system
software depend entirely on the experience and attention of the experts. If the V&V of
the system software is not conducted adequately, overlooked system errors can lead to
downtime for extremely expensive production plants.
Although software plays an ever-increasing role in robotics, current software engi-
neering practices are perceived as insufficient, often leading to error-prone software that
is hard to maintain and cannot easily evolve [
1
]. Moreover, research and industry have
tried to propose many model-driven solutions to engineer the software of robotics systems.
Casalaro et al. [
2
] provide a map of software engineering research in MDE for robotic
systems since there is no systematic study of state-of-the-art developments in model-driven
engineering (MDE) for robotic systems. Robotic systems are advanced cyber-physical
systems (CPS) composed of an intricate blend of hardware, software, and environmental
components. Software engineering can be very beneficial in the CPS domain; however,
it has traditionally been considered an auxiliary concern of robotic system construction.
On the other hand, software engineering technologies and methodologies can facilitate
the development of robotic systems by adopting a systematic, disciplined, quantifiable
approach in each phase of a software application’s lifespan, from requirements analysis,
system architecture definition, and component design to code implementation, testing, and
deployment [
3
]. Some studies provide roboticists with methods and tools to easily create
and validate software for robotic systems. Miyazawa et al. [
4
] and Ye et al. [
5
] propose a
Machines 2023, 11, 282. https://doi.org/10.3390/machines11020282 https://www.mdpi.com/journal/machines
