GJK算法的一种特殊情形的形式化验证和应用  

Formal Verification and Application of a Particular Condition of GJK Algorithm

作　　者：安育龙 施智平[1] 叶世伟[2] 李晓娟[1] 张杰[3] 魏洪兴[4] 

机构地区：[1]高可靠嵌入式系统技术北京市工程研究中心电子系统可靠性技术北京市重点实验室/首都师范大学信息工程学院,北京100048 [2]中国科学院研究生院信息科学与工程学院,北京100049 [3]北京化工大学信息科学与技术学院,北京100029 [4]北京航空航天大学机械工程及自动化学院,北京100191

出　　处：《小型微型计算机系统》2015年第2期365-369,共5页Journal of Chinese Computer Systems

基　　金：国际科技合作计划项目(2010DFB10930,2011DFG13000)资助;国家自然科学基金项目(60873006,61070049,61170304,61104035,61373034,61303014)资助;北京市自然科学基金暨北京市教委重点项目(4122017,KZ201210028036)资助;北京市优秀人才培养项目资助;北京市属高校青年拔尖人才培育计划资助

摘　　要：计算几何算法经常用于机器人避碰运动规划等安全攸关领域,对这些算法进行正确性证明非常重要.用形式化方法对算法进行验证是一种十分有效的手段,尤其是定理证明的方法用严格的数学公理和定理推理证明逻辑模型的性质,对所验证的性质而言是完备的.基于GJK算法设计了计算空间两条线段间距离的算法,用定理证明器HOL4对其相关的定义和定理进行形式化定义和证明,进而基于霍尔逻辑完成形式化表示和证明,对该算法的正确性实现了形式化验证.最后,给出了这一经过验证的算法在双臂机器人无碰撞运动规划中的应用.Computational geometry algorithms are commonly used in safety-critical fields like robot collision-free motion planning, so verifying the correctness of these algorithms is vital. Formal method is a very useful approach to verifying algorithms, especially theo- rem proving which is complete to the proof of the properties by strictly reasoning with mathematics axioms and theorems. This paper presents a particular algorithm based on the GJK algorithm with respect to computing the Euclidean distance between two segments in an n-dimension space, and specifies relevant definitions and theorems in HOL4 and then formalizes and proves the algorithm based on Hoare Logic to demonstrate its correctness. In this paper, an application of the verified algorithm in dual-arm robot collision-free mo- tion planning is also presented.

关 键 词：形式化方法 算法验证 机器人规划 定理证明 HOL 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]