| 机器人碰撞检测方法形式化 |
| |
| 引用本文： | 陈善言,关永,施智平,王国辉.机器人碰撞检测方法形式化[J].软件学报,2022,33(6):2246-2263. |
| |
| 作者姓名： | 陈善言 关永 施智平 王国辉 |
| |
| 作者单位： | 首都师范大学 信息工程学院, 北京 100048;首都师范大学 电子系统可靠性与数理交叉学科国家国际科技合作示范型基地, 北京 100048;首都师范大学 信息工程学院, 北京 100048;首都师范大学 电子系统可靠性与数理交叉学科国家国际科技合作示范型基地, 北京 100048;首都师范大学 轻型工业机器人与安全验证北京市重点实验室, 北京 100048;首都师范大学 信息工程学院, 北京 100048;首都师范大学 电子系统可靠性技术北京市重点实验室, 北京 100048;首都师范大学 信息工程学院, 北京 100048;首都师范大学 高可靠嵌入式系统北京市工程研究中心, 北京 100048 |
| |
| 基金项目： | 国家重点研发计划项目(2019YFB1309900); 国家自然科学基金项目(61876111, 61877040, 62002246); 特区项目(18-163-11-ZT-005-038-05); 北京市教委科技计划一般项目(KM201910028005, KM202010028010); 中央支持地方建设-“双一流”建设项目(20531120005) |
| |
| 摘 要： | 为应对更为复杂的任务需求,现代机器人产业发展愈发迅猛.出于协调工作的灵活性、柔顺性以及智能性等多项考虑因素,多臂/多机器人充分发挥了机器人的强大作用,成为现代机器人产业的重要研究热点.在机器人双臂协调运行当中,机械臂之间以及机械臂与外部障碍物之间容易发生碰撞,可能会造成财产损失甚至人员伤亡.对机器人碰撞检测方法进行形式化验证,以球体和胶囊体形式化模型为基础,构建基本几何体单元之间最短距离和机器人碰撞的高阶逻辑模型,证明其相关属性及碰撞条件,建立机器人碰撞检测方法基础定理库,为多机系统碰撞检测算法可靠性与稳定性的验证提供技术支撑和验证框架.
|
| 关 键 词： | 机器人 碰撞检测 形式化方法 定理证明 HOL-Light |
| 收稿时间： | 2021/9/6 0:00:00 |
| 修稿时间： | 2021/10/14 0:00:00 |
Formalization of Collision Detection Method for Robots |
| |
| CHEN Shan-Yan,GUAN Yong,SHI Zhi-Ping,WANG Guo-Hui.Formalization of Collision Detection Method for Robots[J].Journal of Software,2022,33(6):2246-2263. |
| |
| Authors: | CHEN Shan-Yan GUAN Yong SHI Zhi-Ping WANG Guo-Hui |
| |
| Affiliation: | College of Information Engineering, Capital Normal University, Beijing 100048, China;International Science and Technology Cooperation Base of Electronic System Reliability and Mathematical Interdisciplinary, Capital Normal University, Beijing 100048, China;College of Information Engineering, Capital Normal University, Beijing 100048, China;International Science and Technology Cooperation Base of Electronic System Reliability and Mathematical Interdisciplinary, Capital Normal University, Beijing 100048, China;Beijing Key Laboratory of Light Industrial Robots and Safety Verification, Capital Normal University, Beijing 100048, China;College of Information Engineering, Capital Normal University, Beijing 100048, China;Beijing Key Laboratory of Electronic System Reliability Technology, Capital Normal University, Beijing 100048, China; College of Information Engineering, Capital Normal University, Beijing 100048, China;Beijing Engineering Research Center of High Reliable Embedded System, Capital Normal University, Beijing 100048, China |
| |
| 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 paper, 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. |
| |
| Keywords: | robotics collision detection formal method theorem proving HOL-Light |
|
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
|
