Formalization of robot collision detection method based on conformal geometric algebra
摘要
Cooperative robots can significantly assist people in their productive activities, improving the quality of their works. The normal operation of cooperative robots depends on the reliability of the system, and collision detection method is an important design to achieve this goal. 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 method. This paper builds formal models of geometric primitives and the robot body in HOL Light. We analyse the shortest distance between geometric primitives and verify their collision determination conditions. Then, we construct a formal verification framework for the robot collision detection method. To verify the flexibility and reliability of the proposed framework, we apply it in the scenario of two single-arm industrial cooperative robots.