Formal verification of synchronization properties of a multi-robot welding system
Abstract
Welding tasks are among the most prevalent use cases of robots. In this thesis, thesynchronization properties of a welding system, the IntelliWelder M06, are formallyverified. The welding system consists of a robotic arm (UR10e) and a welding table(Carpano FIVE MOT) external axis. This system allows the user to define awelding operation directly on a CAD model in simulation and consequently planstrajectories for the robotic arm and external axis so that the welding operation canbe performed autonomously. The relevant sections of this system are modeled usingRoboChart, a UML-based modeling language tailored to represent roboticapplications accurately. This work is performed to verify properties critical to thesynchronized operation of the system through model checking. Desired propertieswere defined as assertions through tock-CSP, a process algebra that includes thetock event representing the passage of discrete time. The assertions required thefollowing properties:• Each time a movement request is received for the robotic arm or the externalaxis, a movement operation is called for the corresponding component.• The state machines corresponding to the system state tracker, the externalaxis, and the robotic arm do not terminate.The CSP refinement checker, FDR4, was used to verify the validity of theseproperties. The results showed that the system requirements were fulfilled for sets ofinputs based on the assumption of correctness outside of the model. Also, they werenot fulfilled if the components outside the model were not assumed to be ideal,which shows that the modeled part of the system is input-dependant.