Formalization of Collision Detection Method for Robots
Author:
Affiliation:

Clc Number:

TP311

  • Article
  • | |
  • Metrics
  • |
  • Reference [30]
  • |
  • Related [20]
  • |
  • Cited by
  • | |
  • Comments
    Abstract:

    In order to cope with the demands of more complex tasks, the development of modern robotics industry becomes rapidly. Considering the flexibility, compliance, and intelligence required for coordinated work, multi-arm/multi-robots give full play to the powerful role of robots and become an important research hotspot in the modern robotics industry. In the coordinated operation of the two arms of the robot, collisions between the robot arms and external obstacles are prone to occur, which may cause property damage and even casualties. In this study, a formal verification of the robot collision detection method is carried out. Based on the formal model of sphere and capsule, the shortest distance model of the robot geometric units and the robotic collision model are established. Meanwhile, its related attributes and the collision conditions have been formally verified. Based on the above content, the basic theorem library of robot collision detection has been successfully established, which provides technical support and method reference for further realizing the reliability and stability verification of the collision detection algorithm of the multi-machine system.

    Reference
    [1] Ren XM, Wang DH. The contemporary development of robots and its ethical issues. Studies in Dialectics of Natural, 2013, 29(6):113-118(in Chinese with English abstract).[doi:10.19484/j.cnki.1000-8934.2013.06.023]
    [2] Zhang X. Four dimensions of network society governance. Chinese Public Administration, 2017(9):32-34(in Chinese with English abstract).[doi:10.3782/j.issn.1006-0863.2017.09.06]
    [3] Lozier DW, Olver FWJ. Numerical evaluation of special functions. In:Gautschi W, ed. AMS Proc. of the Symp. in Applied Mathematics. 2000. 1-48.
    [4] Govindaraju NK, Kabul I, Lin MC, et al. Fast continuous collision detection among deformable models using graphics processors. Computers& Graphics, 2007, 31(1):5-14.
    [5] Wang ZW, Xu H. Collision detection algorithm based on topological space grid in complex scenes. Computer System Application, 2017, 26(12):116-123(in Chinese with English abstract).
    [6] Gilbert EGM, Johnson DW, Keerthi SS. A fast procedure for computing the distance between complex objects in three-dimensional space. IEEE Journal on Robotics and Automation, 1988, 4(2):193-203.
    [7] Jin YX, Qin ZP, Li Z. Deformable body collision detection algorithm fused with R-Sphere bounding sphere. Computer Engineering and Design, 2017, 38(1):92-96(in Chinese with English abstract).
    [8] Harrison J. Formal proof-theory and practice. Notices of the American Mathematical Society, 2008, 55(11):1-2.
    [9] Harrison J. HOL light:An overview. In:Proc. of the 22nd Theorem Proving in Higher Order Logics. Munich:Springer-Verlag, 2009. 60-66. http://dx.doi.org/10.1007/978-3-642-03359-9_4
    [10] Faure F, Barbier S, Allard J, et al. Image-based collision detection and response between arbitrary volume objects. In:Proc. of the 7th ACM SIGGRAPH/Eurographics Symp. on Computer Animation. Eurographics Association, 2008. 155-162.
    [11] Qu HY, Li WH, Zhao W. Human-vehicle collision detection algorithm based on image processing. Int'l Journal of Pattern Recognition and Artificial Intelligence, 2020, 34(8).
    [12] Shen XL, Wang RX. Research on fast collision detection algorithm based on improved particle swarm. Computer Engineering and Applications, 2016, 52(22):49-54(in Chinese with English abstract).
    [13] Zhao L, Zhang YD, Hu XX. Collision detection algorithm for industrial robot simulation based on mesh envelope. China Mechanical Engineering, 2017, 28(3):316-321(in Chinese with English abstract).
    [14] Huang YC, Guo S, Zhang LG. A novel self-collision detection algorithm for dual-arm upper Limb rehabilitation robot based on key point-key line segment model. Int'l Journal of Mechatronics and Applied Mechanics, 2020, 1(7):48-54.
    [15] Liang MD. Research on collision detection technology of space manipulator[MS. Thesis]. Harbin:Harbin Institute of Technology, 2020(in Chinese with English abstract).[doi:10.27061/d.cnki.ghgdu.2020.001000].
    [16] Luckcuck M, Farrell M, Dennis L A, et al. Formal specification and verification of autonomous robotic systems:A survey. ACM Computing Surveys, 2019, 52(5):1-32.
    [17] Affeldt R, Cohen C. Formal foundations of 3D geometry to model robot manipulators. In:Proc. of the 6th ACM SIGPLAN Conf. on Certified Programs and Proofs. New York, 2017. 30-42.
    [18] Chen Q, Wang GH, Zhang QY, Shi ZP, Chen SY, Guan Y. Formal modeling and verification of planar parallel mechanism. Journal of Chinese Computer Systems, 2020, 41(5):925-1031(in Chinese with English abstract).[doi:CNKI:SUN:XXWX.0.2020-05-005]
    [19] Rashid A, Hasan O. Formal analysis of robotic cell injection systems using theorem proving. In:Proc. of the Cyber Physical Systems-Design, Modeling, and Evaluation. Cham, 2019. 127-141.
    [20] Täubig H, Frese U, Hertzberg C, et al. Guaranteeing functional safety:Design for provability and computer-aided verification. Autonomous Robots, 2012, 32:303-331.
    [21] Mitsch S, Ghorbal K, Platzer A. On provably safe obstacle avoidance for autonomous robotic ground vehicles. In:Proc. of the Robotics:Science and Systems IX. 2013. 1-8.
    [22] Harrison J. HOL light:A tutorial introduction. Lecture Notes in Computer Science, 1997, 1166.
    附中文参考文献:
    [1] 任晓明,王东浩.机器人的当代发展及其伦理问题初探.自然辩证法研究, 2013, 29(6):113-118.[doi:10.19484/j.cnki.1000-8934.2013.06.023]
    [2] 张晓.网络社会治理的4个维度.中国行政管理, 2017(9):32-34.[doi:10.3782/j.issn.1006-0863.2017.09.06]
    [5] 王振文,徐华.复杂场景中基于拓扑空间网格的碰撞检测算法.计算机系统应用, 2017, 26(12):116-123.
    [7] 靳雁霞,秦志鹏,李照.融合R-Sphere包围球的变形体碰撞检测算法.计算机工程与设计, 2017, 38(1):92-96.
    [12] 沈学利,王瑞新.基于改进粒子群的快速碰撞检测算法研究.计算机工程与应用, 2016, 52(22):49-54.
    [13] 赵亮,张义德,胡旭晓.基于网格包络的工业机器人仿真碰撞检测算法.中国机械工程, 2017, 28(3):316-321.
    [15] 梁孟德.空间机械臂碰撞检测技术研究[硕士学位论文].哈尔滨:哈尔滨工业大学, 2020.[doi:10.27061/d.cnki.ghgdu.2020. 001000]
    [18] 陈琦,王国辉,张倩颖,施智平,陈善言,关永.平面并联机构的形式化建模与验证.小型微型计算机系统, 2020, 41(5):925-1031.[doi:CNKI:SUN:XXWX.0.2020-05-005]
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

陈善言,关永,施智平,王国辉.机器人碰撞检测方法形式化.软件学报,2022,33(6):2246-2263

Copy
Share
Article Metrics
  • Abstract:1128
  • PDF: 4690
  • HTML: 3827
  • Cited by: 0
History
  • Received:September 06,2021
  • Revised:October 28,2021
  • Online: January 28,2022
  • Published: June 06,2022
You are the first2044692Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063