一个空间线段距离算法的形式化和应用

摘要：

对机器人控制算法进行验证工作,对于保障机器人安全工作具有重要意义.本文给出了一个可以在双臂机器人无碰撞运动规划中应用的空间线段距离算法,并完成了对这个算法正确性的形式化验证.本文中的形式化验证工作在定理证明器HOL4中实现,包括基本几何定义和定理的表示和证明,基于霍尔逻辑将算法表示成待证明的目标以及对这个目标的证明.

关键词： 机器人 无碰撞运动规划 空间线段距离算法 形式化验证

作者: 安育龙 施智平 叶世伟 李晓娟 关永 张杰 魏洪兴

作者单位: 高可靠嵌入式系统技术北京市工程研究中心电子系统可靠性技术北京市重点实验室,首都师范大学信息工程学院,北京100048 中国科学院研究生院信息科学与工程学院,北京100049 北京化工大学信息科学与技术学院,北京100029 北京航空航天大学机械工程及自动化学院,北京100191

会议类型: 国内会议

会议名称: 第八届全国测试学术会议

会议地点: 武汉

会议语种:中文

页码: 313-317

在线出版日期: 2014-07-19（万方平台首次上网日期，不代表论文的发表时间）