| GJK算法的一种特殊情形的形式化验证和应用 |
| |
| 引用本文： | 安育龙,施智平,叶世伟,李晓娟,张杰,魏洪兴.GJK算法的一种特殊情形的形式化验证和应用[J].小型微型计算机系统,2015(2):365-369. |
| |
| 作者姓名： | 安育龙 施智平 叶世伟 李晓娟 张杰 魏洪兴 |
| |
| 作者单位： | 高可靠嵌入式系统技术北京市工程研究中心 电子系统可靠性技术北京市重点实验室,首都师范大学信息工程学院;中国科学院研究生院信息科学与工程学院;北京化工大学信息科学与技术学院;北京航空航天大学机械工程及自动化学院 |
| |
| 基金项目： | 国际科技合作计划项目(2010DFB10930,2011DFG13000)资助;国家自然科学基金项目(60873006,61070049,61170304,61104035,61373034,61303014)资助;北京市自然科学基金暨北京市教委重点项目(4122017,KZ201210028036)资助;北京市优秀人才培养项目资助;北京市属高校青年拔尖人才培育计划资助 |
| |
| 摘 要： | 计算几何算法经常用于机器人避碰运动规划等安全攸关领域,对这些算法进行正确性证明非常重要.用形式化方法对算法进行验证是一种十分有效的手段,尤其是定理证明的方法用严格的数学公理和定理推理证明逻辑模型的性质,对所验证的性质而言是完备的.基于GJK算法设计了计算空间两条线段间距离的算法,用定理证明器HOL4对其相关的定义和定理进行形式化定义和证明,进而基于霍尔逻辑完成形式化表示和证明,对该算法的正确性实现了形式化验证.最后,给出了这一经过验证的算法在双臂机器人无碰撞运动规划中的应用.
|
| 关 键 词： | 形式化方法 算法验证 机器人规划 定理证明 HOL |
| 本文献已被 CNKI 等数据库收录！ |
|
