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

在机器人迅速发展的时代,人机协作型机器人安全性问题是人们关注的焦点.机器人逆运动学的建模与求解是决定其安全性的必要因素之一.旋量法是一种机器人逆运动学建模的常用方法,它可以解决传统D-H参数法的奇异性问题.然而,在建模过程中,旋量法会因人为因素或软件系统缺陷导致模型出现漏洞,从而威胁操作人员安全.因此,本文在旋量高阶逻辑定理证明库的基础上,实现了指数积和Paden-Kahan子问题(subprob-R)等数学理论的高阶逻辑表达,在交互式定理证明器HOL-Light中对6R型协作型机器人逆运动学建模与求解过程进行了形式化验证,结果表明基于旋量理论和Paden-Kahan子问题的协作机器人逆运动学建模与求解是安全可靠的.