用形式化验证发现协作机器人焊接不同步的硬件问题
Model Checking and Verification of Synchronisation Properties of Cobot Welding
- 通过模型检验分析机器人与转台的同步机制
- 发现同步性依赖外部假设，实际硬件存在缺陷
- 指导现场重新校准，显著提升焊接质量
本文采用模型检验技术验证由协作机械臂和外部旋转台组成的工业焊接系统的同步性。机器人需协同运动，但时常出现不同步，导致拐角等区域焊缝质量不佳。此类错误代价高昂，既浪费自动焊接时间，又需人工修复。验证表明，只要模型外部分的正确性假设成立，同步性即可满足，揭示了硬件层面的局限性。该发现明确了问题根源，并促使对实际系统进行重新校准，大幅改善了焊接效果，证明了形式化方法在工业场景中的实用价值。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。