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

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

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.