微信服务号

微信订阅号

2025年5月1日 9:54 星期四
首页 > 过刊浏览>2024年第35卷第9期 >4160-4178. DOI:10.13328/j.cnki.jos.007131
PDF HTML阅读 XML下载 导出引用 引用提醒
基于DH标定的机器人正向运动学形式化验证
作者:
作者简介:

谢果君(1992－), 男, 博士生, CCF学生会员, 主要研究领域为形式化工程数学, 控制系统形式化, 定理证明. ;杨焕焕(1994－), 女, 博士生, 主要研究领域为人工智能, 强化学习, 机器学习, 智能控制系统. ;石正璞(1986－), 男, 博士生, 主要研究领域为形式化工程数学, Coq定理证明, 飞行控制系统, 硬件设计, 嵌入式系统;陈钢(1958－), 男, 博士, 教授, 博士生导师, CCF杰出会员, 主要研究领域为形式化工程数学, Coq 定理证明, 函数式语言, 类型系统, 形式化方法, 控制系统.

通讯作者:

陈钢, E-mail: gangchensh@nuaa.edu.cn


Formal Verification of Robot Forward Kinematics Based on DH Calibration
Author:
  • 摘要
    • | |
  • 访问统计
    • |
  • 参考文献 [38]
    • |
  • 相似文献 [20]
    • | | |
  • 文章评论
    摘要:

    DH坐标系在机器人运动学分析中发挥着重要的作用. 在基于DH坐标系构建的机器人控制系统中, 机器人结构的复杂性使得构建安全的控制系统成为一个难题, 仅依靠人工方法可能导致系统漏洞和安全风险, 从而危及机器人的安全. 形式化方法通过演绎推理与代码抽取实现了对软硬件系统的设计、开发及验证. 基于此, 设计基于DH标定的机器人正向运动学的形式化验证框架. 在Coq中构建机器人运动理论的形式化证明, 并验证控制算法的正确性以确保机器人的运动安全. 首先, 对DH坐标系进行形式化建模, 构建相邻坐标系间转换矩阵的形式化定义, 并验证该转换矩阵与复合螺旋运动的等价性; 其次, 构建机械臂正向运动学的形式化定义, 并对机械臂运动的可分解性进行形式化验证; 再次, 对工业机器人中常见连杆结构及机器人进行形式化建模, 并完成正向运动学的形式化验证; 最后, 实现Coq到OCaml的代码抽取, 并对抽取的代码进行分析与验证.

    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.

    参考文献
    [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]
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

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

复制
分享
文章指标
  • 点击次数:495
  • 下载次数: 2860
  • HTML阅读次数: 1141
  • 引用次数: 0
历史
  • 收稿日期:2023-09-11
  • 最后修改日期:2023-10-30
  • 在线发布日期: 2024-01-05
  • 出版日期: 2024-09-06
文章二维码
友情链接:中国科学院软件研究所中国计算机学会中国科学院国家自然科学基金委员会CCF数字图书馆Int'l J of Softw Info计算机系统应用
您是第19892975位访问者
版权所有：中国科学院软件研究所 京ICP备05046678号-3
地址：北京市海淀区中关村南四街4号,邮政编码：100190
电话：010-62562563 传真：010-62562533 Email：jos@iscas.ac.cn
技术支持：北京勤云科技发展有限公司

京公网安备 11040202500063号