机器人运动学形式化分析及其算法验证

Robots are about to repeat the revolution of personal computers, entering the high-speed development period. As autonomous kinetic machines, most robots are safety-critical systems which must be verified strictly for security and correctness. The traditional testing methods cannot meet the demand of robot safety verification. The research on formal verification of the robot kinematics is in the initial stage, and the research on theorem proving based formal analysis of robot kinematics is still a blank. Aiming at demand of robot kinetic safety, this project researches theories and methods of formal analysis and verification for the screw theory based kinematics and motion planning of robots, include the following aspects: research on the high order logic formal description of the screw theory and development of its theorem library; research on the formalization of the robot kinematics and development of its theorem library; research on formal analysis and verification of robot motion properties based on the Jacobi matrix. Lastly, we will build a set of theories and methods of formal analysis and verification of security of motion mechanisms, and fill the gap of formal verification in the robot field. The research results will enhance to improve the correctness and safety of the robot system design, accelerate the speed of developing robots, therefore promoting faster and better development of robot industry.

机器人即将重复个人电脑崛起的道路，进入高速发展期。作为自主动作的机器，多数机器人是安全攸关系统，必须进行严格的正确性和安全性验证。传统的测试方法不能满足机器人安全性验证需求。国际上对机器人的形式化验证处于起步阶段，基于定理证明的运动学形式化分析尚属空白。本项目针对机器人的运动安全性需求研究基于旋量理论的运动学形式化分析与验证的理论和方法，包括研究旋量理论的高阶逻辑形式化表示并开发定理库；研究机器人运动学理论的形式化表示并开发定理库；研究基于雅可比矩阵的机器人运动特性形式化分析和验证方法；研究机器人运动规划算法的形式化分析和验证方法。本项目可望在基于旋量的运动机构安全性形式化证明理论和方法方面取得突破，填补我国在机器人形式化验证领域的空白。本项目研究成果有助于提高机器人系统设计的正确性和安全性，加快机器人开发速度，促进机器人产业更快更好地发展。

机器人作为智能制造的核心，进入高速发展期。作为自主动作的机器，多数机器人是安全攸关系统，必须进行严格的正确性和安全性验证。传统的测试方法不能满足机器人安全性验证需求。国际上对机器人的形式化验证处于起步阶段，基于定理证明的运动学形式化分析尚属空白。本项目针对机器人的运动安全性需求研究了基于旋量、几何代数等理论的运动学形式化分析与验证的理论和方法.研究了机器人运动学相关的数学理论的高阶逻辑形式化表示并开发定理库,包括旋量代数、几何代数、函数矩阵及其微积分理论、傅里叶变换、分数阶微积分理论；研发了基于旋量代数和几何代数的机器人运动学和运动规划算法的形式化建模和验证方法；提出了基于雅可比矩阵的机器人运动特性形式化分析和验证方法。本项目培养研究生13名，博士生1名；发表论文18篇，其中SCI论文6篇，申请发明专利7项，已授权1项；成果获得2017年度北京市科学技术二等奖。本项目研发的几何代数高阶逻辑定理库被HOL Light系统收录并公开发布。本项目研究成果有助于提高机器人系统设计的正确性和安全性，加快机器人开发速度，促进机器人产业更快更好地发展。