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, the synchronization properties of a welding system, the IntelliWelder M06, are formally verified. 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 a welding operation directly on a CAD model in simulation and consequently plans trajectories for the robotic arm and external axis so that the welding operation can be performed autonomously. The relevant sections of this system are modeled using RoboChart, a UML-based modeling language tailored to represent robotic applications accurately. This work is performed to verify properties critical to the synchronized operation of the system through model checking. Desired properties were defined as assertions through tock-CSP, a process algebra that includes the tock event representing the passage of discrete time. The assertions required the following properties: • Each time a movement request is received for the robotic arm or the external axis, a movement operation is called for the corresponding component. • The state machines corresponding to the system state tracker, the external axis, and the robotic arm do not terminate. The CSP refinement checker, FDR4, was used to verify the validity of these properties. The results showed that the system requirements were fulfilled for sets of inputs based on the assumption of correctness outside of the model. Also, they were not 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.