Formal analysis of the kinematic Jacobian in screw theory
Formal analysis of the kinematic Jacobian in screw theory
复制标题
螺旋理论中运动学雅可比行列式的形式分析
DOI：
10.1007/s00165-018-0468-0
复制
发表时间：
2018
影响因子：
1
通讯作者：
Song Xiaoyu
中科院分区：
文献类型：
--
作者：
Shi Zhiping;Wu Aixuan;Yang Xiumei;Guan Yong;Li Yongdong;Song Xiaoyu
随着机器人系统的蓬勃发展，可靠性已成为人机关系中最重要的话题。螺旋理论中的雅可比矩阵是机械臂设计与优化的基础。用雅可比矩阵描述了机械臂的灵巧性和奇异性等核心特性。准确的雅可比矩阵规范和严谨的雅可比矩阵分析是保证正确评价机械臂运动性能的必要条件。本文利用高阶逻辑定理证明器HOL4，给出了螺旋理论中雅可比矩阵的形式化分析方法。利用指数积公式和泛函矩阵理论实现了扭转和正运动学的形式化。据我们所知，这项工作是第一次使用定理证明来正式分析运动学雅可比矩阵。通过对Stanford机械手的形式化建模和分析，验证了该方法对机器人机械手运动特性形式化验证的有效性和适用性。
As robotic systems flourish, reliability has become a topic of paramount importance in the human–robot relationship. The Jacobian matrix in screw theory underpins the design and optimization of robotic manipulators. Kernel properties of robotic manipulators, including dexterity and singularity, are characterized with the Jacobian matrix. The accurate specification and the rigorous analysis of the Jacobian matrix are indispensable in guaranteeing correct evaluation of the kinematics performance of manipulators. In this paper, a formal method for analyzing the Jacobian matrix in screw theory is presented using the higher-order logic theorem prover HOL4. Formalizations of twists and the forward kinematics are performed using the product of exponentials formula and the theory of functional matrices. To the best of our knowledge, this work is the first to formally analyze the kinematic Jacobian using theorem proving. The formal modeling and analysis of the Stanford manipulator demonstrate the effectiveness and applicability of the proposed approach to the formal verification of the kinematic properties of robotic manipulators.