Cobot焊接系统同步属性的模型检查与验证

本文描述了使用模型检查来验证由协作机械臂和外部转台组成的工业焊接系统的同步属性。机器人必须同步移动，但有时会失去同步，导致在拐角等问题区域出现质量不佳的焊接结果。这些错误代价高昂，因为既要浪费机器人焊接时间，又要花费人工维修时间来改善焊接质量。同步属性的验证表明，只要关于模型之外部分的正确性假设成立，同步属性即被满足，这表明硬件存在局限性。这些结果指明了问题的根源，促使对实际系统进行再校准。这大大提高了焊接质量，展示了形式化方法在工业环境中的实际应用价值。