基于DH标定的机器人正向运动学形式化验证  

Formal Verification of Robot Forward Kinematics Based on DH Calibration

作　　者：谢果君 杨焕焕 石正璞 陈钢 XIE Guo-Jun;YANG Huan-Huan;SHI Zheng-Pu;CHEN Gang(College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 211106,China;College of Computer Science and Technology,National University of Defense Technology,Changsha 410073,China)

机构地区：[1]南京航空航天大学计算机科学与技术学院,江苏南京211106 [2]国防科技大学计算机学院,湖南长沙410073

出　　处：《软件学报》2024年第9期4160-4178,共19页Journal of Software

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

关 键 词：机器人运动学 形式化验证 DH坐标系 代码自动生成 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]