协作机器人逆运动学形式化建模与验证  

Formal Modeling and Verification of the Inverse Kinematics of Collaborative Robot

作　　者：王畅 王国辉[1] 施智平[1] 关永[1] 张倩颖[1] 邵振洲 WANG Chang;WANG Guo-hui;SHI Zhi-ping;GUAN Yong;ZHANG Qian-ying;SHAO Zhen-zhou(Information Engineering College,Capital Normal University,Beijing 100048,China)

机构地区：[1]首都师范大学信息工程学院,北京100048

出　　处：《小型微型计算机系统》2021年第7期1353-1359,共7页Journal of Chinese Computer Systems

基　　金：国家重点研发计划项目(2019YFB1309900)资助;国家自然科学基金项目(61876111,61877040,62002246)资助;特区项目(18-163-11-ZT-005-038-05)资助;北京市教委科技计划一般项目(KM20190028005)资助;科技创新服务能力建设-基本科研业务费(科研费)项目(006195305000)资助。

摘　　要：在机器人迅速发展的时代,人机协作型机器人安全性问题是人们关注的焦点.机器人逆运动学的建模与求解是决定其安全性的必要因素之一.旋量法是一种机器人逆运动学建模的常用方法,它可以解决传统D-H参数法的奇异性问题.然而,在建模过程中,旋量法会因人为因素或软件系统缺陷导致模型出现漏洞,从而威胁操作人员安全.因此,本文在旋量高阶逻辑定理证明库的基础上,实现了指数积和Paden-Kahan子问题(subprob-R)等数学理论的高阶逻辑表达,在交互式定理证明器HOLLight中对6R型协作型机器人逆运动学建模与求解过程进行了形式化验证,结果表明基于旋量理论和Paden-Kahan子问题的协作机器人逆运动学建模与求解是安全可靠的.In the age of rapid development of robots,the safety of human-machine collaboration is the focus of people’s attention.The modeling and solving of robotic inverse kinematics are the necessary factors which determine the safety of robots.A common method for inverse kinematics solution of robots is screw theory.It avoids the singularity problem which traditional Denavit-Hartenberg parameters(D-H parameters)can not.However,in the use of the screw theory,there will be some loopholes in the model due to human factors or software defects.Therefore,it is necessary to introduce formal method based on theorem proving to verify the model of robotic inverse kinematics.For this purpose,some basic concepts such as exponential products and Paden-Kahan subproblems(subprob-R)are formalized based on the library of screw theory.And then,the inverse kinematics of collaborative robots is formally verified in HOL-Light.It is proved that Paden-Kahan subproblems(subprob-R)based inverse kinematics of collaboration is safe and reliable.

关 键 词：机器人逆运动学 旋量 Paden-Kahan子问题 HOL-Light 形式化验证 

分 类 号：TP302[自动化与计算机技术—计算机系统结构]