Pith. sign in

REVIEW 3 major objections 6 minor 26 references

Model Checking and Verification of Synchronisation Properties of Cobot Welding

T0 review · 3 major / 6 minor · reviewed 2026-08-12 · deepseek-v4-flash

Pith's one-line read The paper claims that model checking a cobot welding cell's movement-dispatch software shows synchronisation holds only when non-negative time budgets are assumed; allowing negative budgets makes six of seven assertions fail, revealing…

desk verdict A solid machine-checked case study whose real result is 'the model flags negative time budgets', not 'the hardware is miscalibrated'. read the letter →

arxiv 2411.14369 v1 pith:4N7RMQSF submitted 2024-11-21 cs.RO cs.MAcs.SE

classification cs.ROcs.MAcs.SE
keywords modelcheckingsynchronisationcobotweldingexternalaxisRoboCharttock-CSPFDRindustrialformalverification
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper reports a model-checking case study on an industrial cobot welding cell in which a robot arm and an external turntable must move synchronously around corners but sometimes fall out of sync, producing defective welds. It builds a RoboChart model of the control software that receives movement requests, selects movement commands, and detects when a request arrives with a target time already in the past. Seven assertions are checked in FDR under two assumptions: with only non-negative time budgets all assertions pass, while with negative budgets allowed six of seven fail. The authors take this contrast as evidence that the real hardware cannot follow the nominal planned trajectories, and report that recalibrating the physical system drastically improved weld quality. The claim is conditional: synchronisation is verified provided assumptions about correct execution outside the model hold.

What carries the argument

The load-bearing object is the controller model in RoboChart, a domain-specific modelling language for robotic systems: five parallel state machines (System, UR, EXAX, an out_of_sync relay, and a guard machine state_check) that decide whether each movement request is forwarded and which UR movement type is used. The decisive knob is the integer range core_int for the time variable: [0..2] makes late waypoints impossible, while [-1..1] allows a negative time budget that triggers an out_of_sync event. The verification runs on FDR using tock-CSP assertions, including an ADeadline construct from the tock-CSP mechanisation that forces the corresponding move operation to be called immediately upon each move event; the pass/fail pattern across the two ranges is what localises the fault.

What would settle it

Record the time budget (target time minus arrival time) for every waypoint on the real system over many welds, before and after recalibration; if negative budgets largely disappear after recalibration and weld quality improves, the hardware diagnosis is confirmed. If negative budgets persist after recalibration, or appear in a test with known-good calibrated hardware and nominal trajectories, then the unmodelled assumptions about execution, communication, or trajectory feasibility are what the model is actually detecting.

Watch

Extended reading notes

Core claim

The paper's central claim is that the synchronisation logic of the welding system is correct as designed, and that the observed weld defects come from the physical hardware falling behind the nominal plan. This is established by checking seven tock-CSP assertions against a RoboChart model of the movement-dispatch software. With the time-budget range restricted to non-negative values ([0..2]), all assertions pass, meaning every movement request is answered immediately by a movement command and neither robot state machine terminates. With negative budgets allowed ([-1..1]), assertions A1–A6 fail and only A7 passes, giving counterexample traces in which an out_of_sync event occurs and the UR and EXAX machines fail to terminate as required. The authors read this as showing that the modelled software detects and reports out-of-sync conditions, while the real system's inability to stay on schedule is the source of the defects; re-calibration of the physical cell subsequently improved weld quality.

Load-bearing premise

The conclusion that hardware is at fault rests on assuming that everything outside the modelled dispatch software—the robots' actual execution of movement commands, communication delays, and the offline trajectory planner's output—is correct; if any of those parts err, the negative budgets that make the realistic-case assertions fail could originate there instead of in hardware calibration.

Editorial extensions

If this is right

  • If the central claim is correct, the movement-dispatch software is not the cause of the bad welds: under feasible nominal plans it always answers every movement request with a movement command and never terminates prematurely.
  • The model gives a precise failure signature for out-of-sync conditions—a negative time budget triggering the out_of_sync event—so weld defects can be diagnosed by looking at time budgets rather than by inspecting weld beads.
  • The two-range verification becomes a reusable regression test: after any change to the dispatch software, both core_int ranges should reproduce the same pass/fail pattern for A1–A7.
  • The reported recalibration success is a practical corollary: if the hardware is the limiting factor, restoring the physical alignment between the CAD model and the real cell should restore synchronisation.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The same split of time-budget ranges could be applied per robot rather than globally, so failures of A1/A3 but not A2/A4 would identify whether the arm or the turntable is the late partner.
  • Because the model assumes the offline trajectory planner's waypoint plans are feasible, feeding actual waypoint timings into the model would test whether some bad welds come from infeasible acceleration or speed demands rather than from calibration.
  • A production monitor that logs the sign of each time budget could turn the model's out_of_sync event into a live alert; if negative budgets cluster at corners, that would point to acceleration limits as the hardware constraint.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 6 minor

Summary. The paper reports an industrial case study in which the authors model the controller of a cobot welding system (a UR10e robot and a Carpano FIVE turntable) in RoboChart, translate it to tock-CSP via RoboTool, and use FDR to verify synchronisation properties. Seven assertions A1-A7 are checked under two time-budget ranges: core_int=[0..2] (nominal case, no negative budgets) and core_int=[-1..1] (realistic case, negative budgets possible). In the nominal case all assertions pass; in the realistic case all but A7 fail. The authors interpret this difference as evidence that the real robots cannot follow the nominal plans, indicating hardware limitations, and they report that a subsequent recalibration of the system drastically improved weld quality.

Significance. The paper is a valuable experience report if its causal conclusion is appropriately qualified. Its concrete strengths are that the assertions are written as independent user-specified tock-CSP properties, the FDR checks are machine-run with reproducible timing and state-space statistics in Tables 1 and 2, and the model's scope and abstractions are stated explicitly. The modelling pattern for out-of-sync detection and the use of a nominal-versus-realistic value-range comparison are instructive. However, the central inference from the FDR results to a hardware fault is not logically compelled by the presented evidence, and the paper overstates what the verification establishes.

major comments (3)
  1. [Section 5.3 and abstract] The conclusion that the verification results 'indicate limitations in the hardware' is not entailed by the FDR results in Tables 1 and 2. The difference between the two runs is that negative time budgets become possible, and in the model a negative budget triggers out_of_sync and immediate termination of the EXAX/UR machines (Section 4.2). The failures of A1-A6 under core_int=[-1..1] are therefore largely a consequence of how out_of_sync is defined, not a diagnosis of which component produced the negative budget. Section 5.2 itself lists two possible causes: an infeasible plan from Delfoi or incorrect execution by the robot/turntable. The paper provides no evidence ruling out the first cause, since Delfoi trajectory planning is outside the model's scope (Section 4). Please either weaken the claim to 'a problem in the unmodelled context (hardware or planner)' or add supplementary data (e.g., trajectory-feasibility checks, execution timing measurements) that attribute the negative budgets to hardware.
  2. [Section 5.2, assertions A5-A6] Assertions A5 and A6 are stated as 'EXAX does not terminate' and 'UR does not terminate', and the counterexample shown in Fig. 10 is the out_of_sync event that leads to termination. Because the model treats out_of_sync as a critical failure that transitions to the final state, the failed checks under core_int=[-1..1] confirm only that the machines terminate when a negative budget arrives; they do not locate the source of the negative budget. The paper should state this interpretation explicitly and should not use these particular failures as evidence of hardware malfunction.
  3. [Sections 4 and 5.3] The hardware conclusion rests on assumptions that are stated but not discharged: actual execution of move commands is assumed correct, communication delays are assumed negligible, and trajectory feasibility is assumed. The abstract's 'as long as assumptions ... hold' is a conditional, but Section 5.3's 'indicates that the robots are unable to follow the nominal plans' and 'due to hardware limitations' drops that conditional. The manuscript should either frame the conclusion as a hypothesis supported by the engineering outcome (recalibration improving the weld) rather than by the model-checking result alone, or it should specify and carry out a test that distinguishes the two alternatives.
minor comments (6)
  1. [Listing 5] The explanation of SysTerminates says 'hiding all events except System::terminate', but the CSP code shown hides System::terminate; please clarify the hiding/projection semantics, since A7 is the only assertion that passes in both tables and its formulation matters.
  2. [Fig. 10] The counterexample trace is not explained in enough detail; please indicate which event values make the displayed trace a counterexample to A5 (or A6) and how to read the events in the figure.
  3. [Section 4.1] The abstract time-budget values [0..2] and [-1..1] are introduced without stating their relationship to physical time; a sentence explaining the time-unit abstraction would help the reader assess the realism of the ranges.
  4. [Section 3.3.1] The two system-wide requirements are not explicitly linked to R1/R2 and to the verified assertions; an explicit traceability sentence would strengthen the presentation.
  5. [Section 4.2] The out_of_sync Relay state machine is described as 'simple and omitted'; since it is part of the model and affects synchronisation, please include it or give its full definition in an appendix.
  6. [Throughout] The term 'timelock-free' is used without definition; please define it or provide a reference, and unify the spelling of 'SysTerminates' in Listing 5.

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity: the FDR verification is self-contained and tool-checked; the hardware-limitation inference is an interpretation, not a circular derivation.

full rationale

The paper's derivation chain is an industrial case study rather than a fitted prediction: the URScript and PLC behaviour are captured in a RoboChart model, the model is translated to tock-CSP by RoboTool, and assertions A1-A7 are checked by the external model checker FDR. No parameter is fitted to the assertions, and the assertions are user-written specifications independent of the model. The reliance on RoboChart, RoboTool, and tock-CSP is supported by peer-reviewed publications with formal semantics and by an independently implemented checker, so it does not raise the circularity score. The only apparent candidate for circularity is that assertions A5 and A6 fail in the realistic case because the model defines out_of_sync as a negative time budget and makes the EXAX and UR machines terminate on that event; the paper itself says these assertions are 'expected to pass given that no out_of_sync occurs' and treats their failure as showing R1, not as discovering the cause. The inference in Section 5.3 that the failures 'indicate that the robots are unable to follow the nominal plans' goes beyond the model, especially because Section 5.2 explicitly lists an 'infeasible plan from Delfoi' as an equally admissible cause of a negative time budget. That is a scope and evidence concern, rather than a circular step: the FDR results are conditional on the input ranges and do not themselves identify which cause produced a negative budget. The abstract's caveat 'as long as assumptions of correctness made about parts outside the scope of the model hold' is consistent with this conditional character. Overall, no claim in the paper reduces by construction to its inputs or to a self-citation chain.

Assumptions & free parameters 4 free parameters · 5 assumptions · 0 invented entities

The central verification result depends on a small, hand-constrained model of the welding cell. No new physical or mathematical entities are introduced; the load-bearing assumptions are about what lies outside the model: hardware execution correctness, negligible communication delays, feasible trajectories, and the toolchain's soundness. The free parameters are model bounds and thresholds chosen to make the verification tractable, not values fitted to make the assertions pass.

free parameters (4)
  • core_int time budget range = [0..2] nominal, [-1..1] realistic
    Hand-chosen integer abstraction of the time budget for movement requests. The entire differential verification result (Tables 1 vs 2) is produced by toggling between these ranges; the mapping from an abstract negative budget to a real missed deadline is assumed, not measured.
  • waypoint counter maxima = UR [0..3], EXAX [0..1], n_waypoints for EXAX = 1
    Limits state space and encodes that the two axes have different waypoint counts. Assertions A5 and A6 about non-termination are sensitive to these bounds, so the central non-termination results are relative to these small ranges.
  • ADeadline deadline constant = 0 tocks
    Assertions A1 and A3 require the corresponding movement operation to be called before any time passes. This urgency assumption is a specification choice; a larger deadline would change which assertions fail.
  • choose_cmd thresholds = offset threshold 0.8 mm, large-distance threshold 1
    Used to select MoveJ, MoveL, MoveP, or MoveL_with_t in the UR state machine. They do not affect the synchronisation assertions directly but are concrete parameters taken from the use case.
assumptions (5)
  • domain assumption Execution of movement commands by the UR robot and Carpano FIVE is correct and outside the model scope.
    Section 4 states: 'We expect and assume that the actual execution of movement commands by the UR robot and Carpano FIVE is correct.' This is load-bearing for the inference that failures come from planning or hardware rather than from the modelled command selection.
  • domain assumption Communication delays are negligible.
    Section 4 opens with: 'Any possible communication delays are assumed to be handled separately and are hence negligible for our purposes here.' If real RTDE or PLC communication delays are significant, the negative time budgets could have a different cause.
  • domain assumption Trajectory planning is outside scope and planned trajectories are feasible.
    Section 4 states that trajectory planning is outside the model's scope and the feasibility of planned trajectories is assumed. In the realistic case, a negative time budget could therefore also indicate an infeasible Delfoi plan, which the paper itself mentions in Section 5.2.
  • domain assumption RoboChart semantics and RoboTool's tock-CSP translation correctly represent the state machines.
    The verification relies on the soundness of the RoboChart-to-CSP toolchain. The paper cites [2] for sound reasoning in tock-CSP but does not independently justify the translation for this model.
  • domain assumption Model abstractions (two joints, small value ranges, omitted variables) preserve the synchronisation-relevant behaviour.
    Section 4.1 justifies these as state-space reductions, but no validation against the real system is shown. The 'reality gap' is acknowledged in Section 6 as a key limitation.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Model Checking and Verification of Synchronisation Properties of Cobot Welding." pith.science (2026). https://pith.science/paper/4N7RMQSF

@misc{pith2026241114369,
  author       = {Pith},
  title        = {Pith review of: Model Checking and Verification of Synchronisation Properties of Cobot Welding},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/4N7RMQSF}},
  note         = {Machine review of arXiv:2411.14369}
}
read the original 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.

Figures

Figures reproduced from arXiv: 2411.14369 by the authors.

Figure 1
Figure 1. The IntelliWelder system with the different components marked by number [16] [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
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. RoboChart [14], a domain-specific language for modelling and verification of robotic systems. Using our RoboChart model, key synchronisation properties have been verified using the refinement model checker FDR [25]. Details omitted here are in [16]; the work demonstrates ho… view at source ↗
Figure 3
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. The waypoint paths generated in Delfoi are transferred to the Industrial PC (IPC). The waypoints are then processed to convert them into trajectories based on the desired forward welding speed and other [PIT… view at source ↗
Figures from the paper (8 more)
Figure 4
Figure 4. Figure 4: shows the robotic platform of our model (on the right), with three input events (start_system, next_UR_move and next_EXAX_move) and the five operations that can be called (four operations in ur_ops and one in exax_ops). The events, declared in the events interface, are…
Figure 5
Figure 5. Figure 5: Main module including the Controller with all state machines and the robotic platform. by events UR_done and EXAX_done, or an out_of_sync event occurs. An out_of_sync event, from any of the states working, UR_finished or EXAX_finished, results in a transition to the fi…
Figure 6
Figure 6. Figure 6: System state machine. System state machine via its event EXAX_done. (System then transitions to its state EXAX_finished). The UR state machine It is defined in [PITH_FULL_IMAGE:figures/full_fig_p009_6.png]
Figure 7
Figure 7. Figure 7: EXAX state machine that choose_cmd is exited. If the offset is large, the next junction checks whether the move request contains a sharp corner or not (ur_move.sharp_corner). If it does not, moveP is suitable, but if it does, it is necessary to use moveL_with_t. In eac…
Figure 8
Figure 8. Figure 8: UR state machine. 5 Model Checking In this section, we describe the model checking and its results: the defined properties and assertions (Sec￾tion 5.1), the results from FDR (Section 5.2), and their implications for the real-life system (Section 5.3). 5.1 Verification…
Figure 9
Figure 9. Figure 9: State machine responsible for relaying the move commands of the UR and EXAX only if System is in a state where those state machines should receive commands. All the assertions described above are detailed next. Assertion A1 We present in Listing 1 the RoboTool script d…
Figure 10
Figure 10. Figure 10: Trace showing a counterexample to assertion A5 - EXAX does not terminate [PITH_FULL_IMAGE:figures/full_fig_p015_10.png]
Figure 11
Figure 11. Figure 11: A corner of the workpiece showing significantly improved welding quality after system re-calibration. 6 Conclusion and Further Work Applying model checking to an already existing industrial robotic system with known weaknesses has proved to be both challenging and use…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

26 extracted references · 17 canonical work pages

  1. [16]

    Master’s thesis, Norwegian University of Life Sciences, Ås, Norway

    Henrik Nordlie (2024): Formal verification of synchronization properties of a multi-robot welding system . Master’s thesis, Norwegian University of Life Sciences, Ås, Norway. 108 Model Checking and Verification of Synchronisation Properties of Cobot Welding

  2. [1]

    MIT Press

    Christel Baier & Joost-Pieter Katoen (2008): Principles of model checking. MIT Press

  3. [2]

    Baxter, P

    J. Baxter, P. Ribeiro & A. L. C. Cavalcanti (2022): Sound reasoning in tock-CSP. Acta Informatica 59, pp. 125–162, doi:10.1007/s00236-020-00394-3

  4. [3]

    A. L. C. Cavalcanti, A. C. A. Sampaio, A. Miyazawa, P. Ribeiro, M. Conserva Filho, A. Didier, W. Li & J. Timmis (2019): Verified simulation for robotics. Science of Computer Programming 174, pp. 1–37, doi:10.1016/j.scico.2019.01.004. Available at papers/CSMRCD19.pdf

  5. [4]

    Springer International Publishing, doi:10.1007/978-3-030-66494-7_9

    Ana Cavalcanti, Will Barnett, James Baxter, Gustavo Carvalho, Madiel Conserva Filho, Alvaro Miyazawa, Pedro Ribeiro & Augusto Sampaio (2021): RoboStar Technology: A Roboticist’s Toolbox for Combined Proof, Simulation, and Testing. Springer International Publishing, doi:10.1007/978-3-030-66494-7_9

  6. [5]

    In: Software Engineering for Robotics , Springer, doi:10.1007/978-3-030- 66494-7_9

    Ana Cavalcanti, Will Barnett, James Baxter, Gustavo Carvalho, Madiel Conserva Filho, Alvaro Miyazawa, Pedro Ribeiro & Augusto Sampaio (2021): RoboStar Technology: A Roboticist’s Toolbox for Combined Proof, Simulation, and Testing . In: Software Engineering for Robotics , Springer, doi:10.1007/978-3-030- 66494-7_9. Available at https://link.springer.com/10...

  7. [6]

    (2021):On the use of simulation in robotics: Oppor- tunities, challenges, and suggestions for moving forward

    HeeSun Choi, Cindy Crump, Christian Duriez, Asher Elmquist, Gregory Hager, David Han, Frank Hearl, Jessica Hodgins, Abhinandan Jain, Frederick Leve et al. (2021):On the use of simulation in robotics: Oppor- tunities, challenges, and suggestions for moving forward. Proceedings of the National Academy of Sciences 118, doi:10.1073/pnas.1907856118

  8. [7]

    Clarke (1997): Model checking

    Edmund M. Clarke (1997): Model checking . In: Foundations of Software Technology and Theoreti- cal Computer Science , 1346, Springer Berlin Heidelberg, doi:10.1007/BFb0058022. Available at http: //link.springer.com/10.1007/BFb0058022

Show all 26 references
  1. [8]

    In: ASME international mechanical engineering congress and exposition , 15281, American Society of Mechanical Engineers, doi:10.1115/IMECE1996-0367

    J Edward Colgate, Witaya Wannasuphoprasit & Michael A Peshkin (1996):Cobots: Robots for collaboration with human operators . In: ASME international mechanical engineering congress and exposition , 15281, American Society of Mechanical Engineers, doi:10.1115/IMECE1996-0367

  2. [9]

    Available at http://www.eclipse.org/

    Eclipse Foundation (visited August 5, 2024): Eclipse website. Available at http://www.eclipse.org/

  3. [10]

    Roscoe (2014): FDR3 — A Modern Refinement Checker for CSP

    Thomas Gibson-Robinson, Philip Armstrong, Alexandre Boulgakov & Andrew W. Roscoe (2014): FDR3 — A Modern Refinement Checker for CSP . In: Tools and Algorithms for the Construction and Analysis of Systems, Springer Berlin Heidelberg, doi:10.1007/978-3-642-54862-8_13

  4. [11]

    C. A. R. Hoare (1978): Communicating sequential processes . Communications of the ACM 21, doi:10.1145/359576.359585. Available at https://dl.acm.org/doi/10.1145/359576.359585

  5. [12]

    International journal of mechanical and materials engineering10, doi:10.1186/s40712- 015-0042-y

    P Kah, M Shrestha, E Hiltunen & J Martikainen (2015): Robotic arc welding sensors and programming in in- dustrial applications. International journal of mechanical and materials engineering10, doi:10.1186/s40712- 015-0042-y

  6. [14]

    Software & Systems Modeling 18, doi:10.1007/s10270-018-00710-z

    Alvaro Miyazawa, Pedro Ribeiro, Wei Li, Ana Cavalcanti, Jon Timmis & Jim Woodcock (2019):RoboChart: modelling and verification of the functional behaviour of robotic applications . Software & Systems Modeling 18, doi:10.1007/s10270-018-00710-z. Available at http://link.springe...

  7. [15]

    Anisi & Morten Mossige (2022): Safety assur- ance of an industrial robotic control system using hardware/software co-verification

    Yvonne Murray, Martin Sirevåg, Pedro Ribeiro, David A. Anisi & Morten Mossige (2022): Safety assur- ance of an industrial robotic control system using hardware/software co-verification . Science of Computer Programming 216, doi:10.1016/j.scico.2021.102766. Available at https:/...

  8. [17]

    Available at https: //www.pioneer-robotics.no/cobot/intelliwelder/

    Pioneer Robotics AS (visited August 15, 2024): IntelliWelder - UR+ certified product. Available at https: //www.pioneer-robotics.no/cobot/intelliwelder/

  9. [18]

    Springer Science & Business Media, doi:10.1007/1-84628-191-1

    J Norberto Pires, Altino Loureiro & Gunnar Bölmsjo (2006): Welding robots: technology, system issues and application. Springer Science & Business Media, doi:10.1007/1-84628-191-1

  10. [19]

    IEEE Access 5, doi:10.1109/ACCESS.2017.2708127

    Gang Ren, Qingsong Hua, Pan Deng, Chao Yang & Jianwei Zhang (2017): A Multi-Perspective Method for Analysis of Cooperative Behaviors Among Industrial Devices of Smart Factory . IEEE Access 5, doi:10.1109/ACCESS.2017.2708127

  11. [20]

    Pedroza Yanez & Luz M

    Günther Starke, Daniel Hahn, Diana G. Pedroza Yanez & Luz M. Ugalde Leal (2016): Self-organization and self-coordination in welding automation with collaborating teams of industrial robots . Machines (Basel) 4, doi:10.3390/machines4040023

  12. [21]

    Available at https://thgautomation.com/2024/06/27/in-sync-the-benefits-of-coordinated-motion/

    THG Automation (visited August 19, 2024): In Sync: The Benefits of Coordinated Motion . Available at https://thgautomation.com/2024/06/27/in-sync-the-benefits-of-coordinated-motion/

  13. [22]

    Available at https://www

    Universal Robots (visited August 5, 2024): Universal Robots - UR10e Website. Available at https://www. universal-robots.com/products/ur10-robot/

  14. [23]

    Avail- able at https://www.universal-robots.com/articles/ur/interface-communication/ real-time-data-exchange-rtde-guide/

    Universal Robots (visited August 8, 2024): Real-Time Data Exchange Guide . Avail- able at https://www.universal-robots.com/articles/ur/interface-communication/ real-time-data-exchange-rtde-guide/

  15. [24]

    Avail- able at https://www.universal-robots.com/download/manuals-e-seriesur20ur30/user/ur10e/ 59/user-manual-ur10e-e-series-sw-59-english-international-en/

    Universal Robots (visited July 23, 2024): Universal Robots e-Series User Manual . Avail- able at https://www.universal-robots.com/download/manuals-e-seriesur20ur30/user/ur10e/ 59/user-manual-ur10e-e-series-sw-59-english-international-en/

  16. [25]

    https://cocotec

    University of Oxford (visited August 15, 2024): FDR4 - The CSP Refinement Checker. https://cocotec. io/fdr/. Available at https://cocotec.io/fdr/

  17. [26]

    Available at https://www

    Visual Components (visited August 15, 2024): Robot Offline Programming. Available at https://www. visualcomponents.com/products/robot-offline-programming/

  18. [27]

    In: Intelligent Robotics and Applications, 13014, Springer, doi:10.1007/978-3-030-89098-8_66

    Jiahao Xiong, Zhongtao Fu, Miao Li, Zhicheng Gao, Xiaozhi Zhang & Xubing Chen (2021): Trajectory- Smooth Optimization and Simulation of Dual-Robot Collaborative Welding . In: Intelligent Robotics and Applications, 13014, Springer, doi:10.1007/978-3-030-89098-8_66

Pith tools

Reviewed August 12, 2026 · model on record in the stance chip above.