软件学报

作者：陈善言，关永，施智平，王国辉

单位：陈善言，首都师范大学 信息工程学院, 北京 100048;电子系统可靠性与数理交叉学科国家国际科技合作示范型基地(首都师范大学), 北京 10004811,关永，首都师范大学 信息工程学院, 北京 100048;电子系统可靠性与数理交叉学科国家国际科技合作示范型基地(首都师范大学), 北京 100048;轻型工业机器人与安全验证北京市重点实验室(首都师范大学), 北京 10004802,施智平，首都师范大学 信息工程学院, 北京 100048;电子系统可靠性技术北京市重点实验室(首都师范大学), 北京 10004803,王国辉，首都师范大学 信息工程学院, 北京 100048;高可靠嵌入式系统北京市工程研究中心(首都师范大学), 北京 10004804

关键词：机器人;碰撞检测;形式化方法;定理证明;HOL-Light

基金：国家重点研发计划(2019YFB1309900);国家自然科学基金(61876111,61877040,62002246);特区项目(18-163-11-ZT-005-038-05);北京市教委科技计划(KM201910028005,KM202010028010);中央支持地方建设——“双一流”建设项目(20531120005)

为应对更为复杂的任务需求,现代机器人产业发展愈发迅猛.出于协调工作的灵活性、柔顺性以及智能性等多项考虑因素,多臂/多机器人充分发挥了机器人的强大作用,成为现代机器人产业的重要研究热点.在机器人双臂协调运行当中,机械臂之间以及机械臂与外部障碍物之间容易发生碰撞,可能会造成财产损失甚至人员伤亡.对机器人碰撞检测方法进行形式化验证,以球体和胶囊体形式化模型为基础,构建基本几何体单元之间最短距离和机器人碰撞的高阶逻辑模型,证明其相关属性及碰撞条件,建立机器人碰撞检测方法基础定理库,为多机系统碰撞检测算法可靠性与稳定性的验证提供技术支撑和验证框架.

来源：2022年第6期

《软件学报》期刊编辑部

查看软件学报杂志2022年第6期