<p>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.</p>

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Formalization of robot collision detection method based on conformal geometric algebra

  • Yingjie Wu,
  • Guohui Wang,
  • Shanyan Chen,
  • Zhiping Shi,
  • Yong Guan,
  • Ximeng Li

摘要

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.