微信服务号

微信订阅号

2025-4-24- 19
Home > Archive>Volume 35, Issue 9, 2024 >4160-4178. DOI:10.13328/j.cnki.jos.007131
PDF HTML XML Export Cite reminder
Formal Verification of Robot Forward Kinematics Based on DH Calibration
Author:
Affiliation:

  • Article
    • | |
  • Metrics
    • |
  • Reference [38]
    • |
  • Related [20]
    • | | |
  • Comments
    Abstract:

    The DH coordinate system plays a vital role in analyzing robot kinematics. In the robot control system built upon the DH coordinate system, the robot structure complexity poses challenges to developing a secure control system. Depending solely on manual methods can introduce system vulnerabilities and security hazards, thereby endangering the overall safety of the robot. The formal method becomes a promising direction to design, develop, and verify hardware and software systems by deductive reasoning and code extraction. Based on this, this study designs a formal verification framework for robot forward kinematics based on the DH calibration, during which the robot kinematics theory is rigorously proven and the correctness of the control algorithm in Coq is verified to ensure the motion safety of the robot. First, it formally models the DH coordinate system, defines the transformation matrix among adjacent coordinate systems, and verifies the equivalence of this transformation matrix with the composite helical motion. Then, the forward kinematics of the robotic arm is formally defined, with its motion detachability verified. Subsequently, this study formally models the common connecting rod structures and robots in industrial robots and verifies their forward kinematics. Finally, the code extraction from Coq to OCaml is implemented, and the extracted code is analyzed and verified.

    Reference
    [1] Hichri B, Gallala A, Giovannini F, Kedziora S. Mobile robots path planning and mobile multirobots control: A review. Robotica, 2022, 40(12): 4257–4270.
    [2] Tan Y, Ma DF, Qiao L. A formal verification method of compilation based on C safety subset. Wireless Communications and Mobile Computing, 2021, 2021: 8352267.
    [3] Zhou S, Wang JB, Jia J, Zhang C, Wang RX. A formal verification method for the SOPC software. IEEE Trans. on Reliability, 2022, 71(2): 818–829.
    [4] Schreiber LT, Gosselin C. Determination of the inverse kinematics branches of solution based on joint coordinates for universal robots-like serial robot architecture. Journal of Mechanisms and Robotics, 2022, 14(3): 034501.
    [5] Elqortobi M, El-Khouly W, Rahj A, Bentahar J, Dssouli R. Verification and testing of safety-critical airborne systems: A model-based methodology. Computer Science and Information Systems, 2020, 17(1): 271–292.
    [6] Sakaguchi K. Program extraction for mutable arrays. Science of Computer Programming, 2020, 191: 102372.
    [7] Annenkov D, Milo M, Nielsen JB, Spitters B. Extracting functional programs from Coq, in Coq. Journal of Functional Programming, 2022, 32: e11.
    [8] Vicentini F, Askarpour M, Rossi MG, Mandrioli D. Safety assessment of collaborative robotics through automated formal verification. IEEE Trans. on Robotics, 2020, 36(1): 42–61.
    [9] Isobe Y, Miyamoto N, Ando N, Oiwa Y. Formal modeling and verification of concurrent FSMs: Case study on event-based cooperative transport robots. IEICE Trans. on Information and Systems, 2021, E104-D(10): 1515–1532.
    [10] Lestingi L, Bersani MM, Rossi M. Model-driven development of service robot applications dealing with uncertain human behavior. IEEE Intelligent Systems, 2022, 37(6): 48–56.
    [11] Askarpour M, Mandrioli D, Rossi M, Vicentini F. Formal model of human erroneous behavior for safety analysis in collaborative robotics. Robotics and Computer-integrated Manufacturing, 2019, 57: 465–476.
    [12] Praveen AT, Gupta A, Bhattacharyya S, Muthalagu R. Assuring behavior of multirobot autonomous systems with translation from formal verification to ROS simulation. IEEE Systems Journal, 2022, 16(3): 5092–5100.
    [13] Martin-Martin E, Montenegro M, Riesco A, Rodríguez-Hortalá J, Rubio R. Verification of the ROS NavFn planner using executable specification languages. Journal of Logical and Algebraic Methods in Programming, 2023, 132: 100860.
    [14] Dal Zilio S, Hladik PE, Ingrand F, Mallet A. A formal toolchain for offline and run-time verification of robotic systems. Robotics and Autonomous Systems, 2023, 159: 104301.
    [15] Bohrer R, Tan YK, Mitsch S, Sogokon A, Platzer A. A formal safety net for waypoint-following in ground robots. IEEE Robotics and Automation Letters, 2019, 4(3): 2910–2917.
    [16] Foughali M, Hladik PE. Bridging the gap between formal verification and schedulability analysis: The case of robotics. Journal of Systems Architecture, 2020, 111: 101817.
    [17] Paul S, Cruz E, Dutta A, Bhaumik A, Blasch E, Agha G, Patterson S, Kopsaftopoulos F, Varela C. Formal verification of safety-critical aerospace systems. IEEE Aerospace and Electronic Systems Magazine, 2023, 38(5): 72–88.
    [18] Xie GJ, Yang HH, Deng H, Shi ZP, Chen G. Formal verification of robot rotary kinematics. Electronics, 2023, 12(2): 369.
    [19] López J, Santana-Alonso A, Medina MDC. Formal verification for task description languages. A Petri net approach. Sensors, 2019, 19(22): 4965.
    [20] Sangnier A, Sznajder N, Potop-Butucaru M, Tixeuil S. Parameterized verification of algorithms for oblivious robots on a ring. Formal Methods in System Design, 2020, 56: 55–89.
    [21] Evangelidis A, Parker D. Quantitative verification of Kalman filters. Formal Aspects of Computing, 2021, 33(4–5): 669–693.
    [22] Abd Alrahman Y, Piterman N. Modelling and verification of reconfigurable multi-agent systems. Autonomous Agents and Multi-agent Systems, 2021, 35(2): 47.
    [23] Rashid A, Hasan O. Formal analysis of the continuous dynamics of cyber-physical systems using theorem proving. Journal of Systems Architecture, 2021, 112: 101850.
    [24] Wang GH, Chen SY, Guan Y, Shi ZP, Li XM, Zhang JZ. Formalization of the inverse kinematics of three-fingered dexterous hand. Journal of Logical and Algebraic Methods in Programming, 2023, 133: 100861.
    [25] Murray Y, Sirev?g M, Ribeiro P, Anisi DA, Mossige M. Safety assurance of an industrial robotic control system using hardware/software co-verification. Science of Computer Programming, 2022, 216: 102766.
    [26] Mkaouar H, Zalila B, Hugues J, Jmaiel M. A formal approach to AADL model-based software engineering. Int’l Journal on Software Tools for Technology Transfer, 2020, 22(2): 219–247.
    [27] Sakata K, Fujita S, Sawada K, Iwasawa H, Endoh H, Matsumoto N. Model verification of fallback control system under cyberattacks via UPPAAL. Advanced Robotics, 2023, 37(3): 156–168.
    [28] Menghi C, Tsigkanos C, Askarpour M, Pelliccione P, Vázquez G, Calinescu R, García S. Mission specification patterns for mobile robots: Providing support for quantitative properties. IEEE Trans. on Software Engineering, 2023, 49(4): 2741–2760.
    [29] Arcile J, Devillers R, Klaudel H. VerifCar: A framework for modeling and model checking communicating autonomous vehicles. Autonomous Agents and Multi-agent Systems, 2019, 33(3): 353–381.
    [30] Pek C, Manzinger S, Koschi M, Althoff M. Using online verification to prevent autonomous vehicles from causing accidents. Nature Machine Intelligence, 2020, 2(9): 518–528.
    [31] Kabra A, Mitsch S, Platzer A. Verified train controllers for the federal railroad administration train kinematics model: Balancing competing brake and track forces. IEEE Trans. on Computer-aided Design of Integrated Circuits and Systems, 2022, 41(11): 4409–4420.
    [32] 麻莹莹, 马振威, 陈钢. 基于Coq的分块矩阵运算的形式化. 软件学报, 2021, 32(6): 1882–1909. http://www.jos.org.cn/1000-9825/6255.htm
    Ma YY, Ma ZW, Chen G. Formalization of operations of block matrix based on Coq. Ruan Jian Xue Bao/Journal of Software, 2021, 32(6): 1882–1909 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/6255.htm
    [33] Shi ZP, Chen G. Integration of multiple formal matrix models in Coq. In: Proc. of the 8th Int’l Symp. on Dependable Software Engineering: Theories, Tools, and Applications. Beijing: Springer, 2022. 169–186. [doi: 10.1007/978-3-031-21213-0_11]
    [34] Boldo S, Lelay C, Melquiond G. Coquelicot: A user-friendly library of real analysis for Coq. Mathematics in Computer Science, 2015, 9(1): 41–62.
    [35] Blanqui F, Koprowski A. CoLoR: A Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates. Mathematical Structures in Computer Science, 2011, 21(4): 827–859.
    [36] Pous D. Untyping typed algebras and colouring cyclic linear logic. Logical Methods in Computer Science, 2012, 8(2): 1–21.
    [37] Shi ZP, Xie GJ, Chen G. CoqMatrix: Formal matrix library with multiple models in Coq. Journal of Systems Architecture, 143: 102986. [doi: 10.1016/j.sysarc.2023.102986]
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

谢果君,杨焕焕,石正璞,陈钢.基于DH标定的机器人正向运动学形式化验证.软件学报,2024,35(9):4160-4178

Copy
Share
Article Metrics
  • Abstract:492
  • PDF: 2846
  • HTML: 1127
  • Cited by: 0
History
  • Received:September 11,2023
  • Revised:October 30,2023
  • Online: January 05,2024
  • Published: September 06,2024
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2038222Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address：4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code：100190
Phone：010-62562563 Fax：010-62562533 Email：jos@iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063