Safety Verification of Multiple Industrial Robot Manipulators with Path Conflicts Using Model Checking
Open Access
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
Funding Information
- ECSEL Joint Undertaking (JU) (876852, 120N800)
- Türkiye Bilimsel ve Teknolojik Araştırma Kurumu (876852, 120N800)
This publication has 30 references indexed in Scilit:
- Toward Reliable Autonomous Robotic Assistants Through Formal Verification: A Case StudyIEEE Transactions on Human-Machine Systems, 2015
- Timed automata based motion planning for a self-assembly robot system2014
- Towards temporal verification of swarm robotic systemsRobotics and Autonomous Systems, 2012
- Analysing robot swarm behaviour via probabilistic model checkingRobotics and Autonomous Systems, 2012
- Model Checking Industrial Robot SystemsLecture Notes in Computer Science, 2011
- PRISM 4.0: Verification of Probabilistic Real-Time Systems2011
- Model-checking algorithms for continuous-time markov chainsIEEE Transactions on Software Engineering, 2003
- Timed Automata1999
- Uppaal in a nutshellInternational Journal on Software Tools for Technology Transfer, 1997
- A theory of timed automataTheoretical Computer Science, 1994