| dc.description.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. | |
