Cooperative robots can significantly assist people in their productive activities, improving the quality of their works. Collision detection is vital to ensure the safe and stable operation of cooperative robots in productive activities. As an advanced geometric language, conformal geometric algebra can simplify the construction of the robot collision model and the calculation of collision distance. Compared with the formal method based on conformal geometric algebra, the traditional method may have some defects which are difficult to find in the modelling and calculation. We use the formal method based on conformal geometric algebra to study the collision detection problem of cooperative robots. This paper builds formal models of geometric primitives and the robot body based on the conformal geometric algebra library in HOL Light. We analyse the shortest distance between geometric primitives and prove their collision determination conditions. Based on the above contents, we construct a formal verification framework for the robot collision detection method. By the end of this paper, we apply the proposed framework to collision detection between two single-arm industrial cooperative robots. The flexibility and reliability of the proposed framework are verified by constructing a general collision model and a special collision model for two single-arm industrial cooperative robots.

翻译：协作机器人能够显著辅助人类的生产活动，提升工作质量。碰撞检测对于确保协作机器人在生产活动中的安全稳定运行至关重要。作为一种先进的几何语言，共形几何代数能够简化机器人碰撞模型的构建与碰撞距离的计算。与基于共形几何代数的形式化方法相比，传统方法在建模与计算过程中可能存在难以发现的缺陷。本文采用基于共形几何代数的形式化方法研究协作机器人的碰撞检测问题。基于HOL Light中的共形几何代数库，构建了几何基元及机器人本体的形式化模型，分析了几何基元之间的最短距离并证明了其碰撞判定条件。在此基础上，构建了机器人碰撞检测方法的形式化验证框架。最后，将该框架应用于两台单臂工业协作机器人之间的碰撞检测，通过构建通用碰撞模型与特殊碰撞模型验证了所提框架的灵活性与可靠性。