Model Checking and Verification of Synchronisation Properties of Cobot Welding

TL;DR

This paper demonstrates how model checking can verify and improve the synchronization of a cobot welding system, leading to better weld quality through identifying hardware limitations and system re-calibration.

Contribution

It applies formal verification to an industrial welding system, showing how model checking can identify synchronization issues and guide hardware adjustments for improved performance.

Findings

Synchronization properties are verified under certain assumptions.

Hardware limitations were identified as the cause of synchronization failures.

Re-calibration based on verification results improved welding quality.

Abstract

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.