拉格朗日动力学形式化及其在机器人验证中的应用

As the theoretical foundation for a great number of sub-disciplines of science and engineering, Lagrangian dynamics has extensive applications in science and engineering. Many dynamic systems (e.g., robotic systems) are safety-critical; hence, it is highly beneficial to conduct rigorous verification of these systems, thereby ensuring their correctness and reliability. To enable computerized derivation of theoretical results on Lagrangian dynamics and to conduct formal verification of dynamic systems, the formalization of Lagrangian dynamics is a pre-requisite. Currently, the formalization of mathematics is drawing a high amount of attention on an international scale. However, the formalization of dynamic theory in particular, remains a hitherto unexplored area. In this project, we will investigate the formalization of Lagrangian dynamics using higher-order logics (HOL). Furthermore, we will develop methodologies for the formal analysis and verification of dynamic systems with robotic systems as a specific application domain. The concrete problems we will address include: the formalization of continuous differentiable function spaces, functional analysis and variational methods, and the least action principle; the formalization of the principle of virtual work, D'Alembert's principle, the general equation of dynamics, and Hamilton principle; the formalization of the Lagrangian function and the two types of Lagrangian equations; and the formal analysis and verification of the dynamic design of robotic mechanisms based on Lagrangian dynamics. In this project, we will fill a gap in the formal verification of Lagrangian dynamic systems by developing the first (HOL-based) library of formal definitions and proofs for Lagrangian dynamics, and by implementing a tool kit for the formal analysis and verification of robot dynamics.

拉格朗日动力学是很多学科和工程的基础理论，应用非常广泛。包括机器人系统等很多动力学系统是安全攸关系统，需要进行严格的正确性和可靠性验证。形式化拉格朗日动力学是进行动力学理论推导和动力学系统形式化验证的基础。目前国际上对形式化数学的研究关注度很高，但是动力学理论的形式化尚属空白。本项目研究拉格朗日动力学的高阶逻辑形式化理论，并以机器人为例研究动力学系统的形式化分析与验证的方法，具体包括：连续可微函数空间、泛函与变分、最小作用原理的形式化表达和证明；虚功原理、达朗贝尔原理、动力学普遍方程和哈密顿原理的形式化表达和证明；拉格朗日量、两类拉格朗日方程的形式化表达和证明；基于拉格朗日动力学理论的机器人机构动力学形式化分析与验证方法。本项目将实现国际上第一个拉格朗日动力学高阶逻辑程序库，实现基于拉格朗日动力学的机器人动力学形式化分析与验证的工具包。

为了确保机器人等动力系统设计的正确性，解决传统的测试与仿真等方法的非完备性问题，本项目聚焦拉格朗日动力学相关理论的形式化建模与定理库构建，完成了泛函变分、拉格朗日力学的形式化及在机器人设计中的应用验证，并探索解决完备验证的自动化难题。本项目的主要成果总结如下：.1. 泛函变分的形式化。给出连续函数空间C(s)(s为紧集)的形式化描述，以及基于该函数空间的泛函Fréchet 形式与Gâteaux 形式变分的形式化描述。开发一套泛函变分形式化定理证明库。.2. 拉格朗日力学的形式化。给出机械功、虚功以及理想约束的形式化描述，在此基上实现虚功原理与达朗贝尔原理的形式化描述与证明。建立转动惯量、牛顿运动方程以及欧拉运动方程的形式化描述，进而实现从虚功原理到牛顿运动方程与欧拉运动方程的形式化证明。给出广义坐标、拉格朗日函数与广义力的形式化描述，并实现从虚功原理与达朗贝尔原理到拉格朗日方程的形式化推导。构建一套拉格朗日力学形式化定理证明库。.3. 机器人动力学的形式化。给出广义齐次矩阵、广义齐次向量以及矩阵值函数微分的形式化描述。建立机器人机构的物体速度、空间速度、物体雅可比矩阵以及空间雅可比矩阵的形式化模型，并完成它们之间关系的形式化证明。依据机器人机构的动能与拉格朗日函数进行形式化模型，实现机器人运动方程的形式化推导。为机器人形式化验证提供新的方法和工具。.本项目实现了国际上第一个拉格朗日动力学高阶逻辑程序库，构建基于拉格朗日动力学的机器人动力学形式化分析与验证的定理证明工具包。为机器人动力学设计的正确性验证提供了理论基础和技术手段。