Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Model Checking and Verification of Synchronisation Properties of Cobot Welding

Yvonne Murray, Henrik Nordlie, David A. Anisi, Pedro Ribeiro, Ana Cavalcanti

Abstract

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.

Model Checking and Verification of Synchronisation Properties of Cobot Welding

Abstract

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.

Paper Structure

This paper contains 33 sections, 11 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Formal Verification and Model Checking
  3. IntelliWelder and Synchronous Welding
  4. System Architecture
  5. Existing URScript code
  6. Requirements
  7. System-Wide Requirements
  8. Model Requirements
  9. Modelling in RoboChart
  10. Abstractions and Simplifications
  11. Reduction of number of joints:
  12. Limited value ranges:
  13. Omitted variables:
  14. RoboChart Model
  15. Module
  16. ...and 18 more sections

Figures (11)

  • Figure 1: The IntelliWelder system with the different components marked by number NordlieThesis.
  • Figure 2: Typical welding issue where there is buildup of filler material (A) and coverage is not sufficient (B), creating an irregular and weakened weld.
  • Figure 3: System architecture of the IntelliWelder. The blue dotted line indicates the scope of the RoboChart model: part of the Industrial PC (IPC), the Real-Time Data Exchange (RTDE) for the UR robot, and the URScript.
  • Figure 4: Robotic platform with its defined events, provided operations and custom record types to represent move commands.
  • Figure 5: Main module including the Controller with all state machines and the robotic platform.
  • ...and 6 more figures