Model Checking and Verification of Synchronisation Properties of Cobot Welding

Fuente: arXiv
Gespeichert in:
Bibliographische Detailangaben
Hauptverfasser: Murray, Yvonne, Nordlie, Henrik, Anisi, David A., Ribeiro, Pedro, Cavalcanti, Ana
Format: Preprint
Veröffentlicht: 2024
Schlagworte:
Online-Zugang:
Tags: Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
_version_ 1866917844289060864
author Murray, Yvonne
Nordlie, Henrik
Anisi, David A.
Ribeiro, Pedro
Cavalcanti, Ana
author_facet Murray, Yvonne
Nordlie, Henrik
Anisi, David A.
Ribeiro, Pedro
Cavalcanti, Ana
contents This paper describes use of model checking to verify synchronisation properties of an industrial welding system consisting of a cobot arm and an external turntable. The robots must move synchronously, but sometimes get out of synchronisation, giving rise to unsatisfactory weld qualities in problem areas, such as around corners. These mistakes are costly, since time is lost both in the robotic welding and in manual repairs needed to improve the weld. Verification of the synchronisation properties has shown that they are fulfilled as long as assumptions of correctness made about parts outside the scope of the model hold, indicating limitations in the hardware. These results have indicated the source of the problem, and motivated a re-calibration of the real-life system. This has drastically improved the welding results, and is a demonstration of how formal methods can be useful in an industrial setting.
format Preprint
id arxiv_https___arxiv_org_abs_2411_14369
institution arXiv
publishDate 2024
record_format arxiv
spellingShingle Model Checking and Verification of Synchronisation Properties of Cobot Welding
Murray, Yvonne
Nordlie, Henrik
Anisi, David A.
Ribeiro, Pedro
Cavalcanti, Ana
Robotics
Multiagent Systems
Software Engineering
This paper describes use of model checking to verify synchronisation properties of an industrial welding system consisting of a cobot arm and an external turntable. The robots must move synchronously, but sometimes get out of synchronisation, giving rise to unsatisfactory weld qualities in problem areas, such as around corners. These mistakes are costly, since time is lost both in the robotic welding and in manual repairs needed to improve the weld. Verification of the synchronisation properties has shown that they are fulfilled as long as assumptions of correctness made about parts outside the scope of the model hold, indicating limitations in the hardware. These results have indicated the source of the problem, and motivated a re-calibration of the real-life system. This has drastically improved the welding results, and is a demonstration of how formal methods can be useful in an industrial setting.
title Model Checking and Verification of Synchronisation Properties of Cobot Welding
topic Robotics
Multiagent Systems
Software Engineering
url https://arxiv.org/abs/2411.14369