欢迎您！东篱公司
退出
-
申报数据库
-
立项数据库
-
成果数据库
-
项目获奖数据库
中文摘要：
计算几何算法经常用于机器人避碰运动规划等安全攸关领域,对这些算法进行正确性证明非常重要.用形式化方法对算法进行验证是一种十分有效的手段,尤其是定理证明的方法用严格的数学公理和定理推理证明逻辑模型的性质,对所验证的性质而言是完备的.基于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.
同期刊论文项目
同项目期刊论文
Analysis of the Degradation of MOSFETs in Switching Mode Power Supply by Characterizing Source Oscil
Power supply prognostics and health management of high reliability electronic systems in rugged envi
期刊信息
位置：