拉格朗日力学理论的形式化与机器人动力学形式化分析

第1章绪论 1.1背景 随着全球经济的不断发展，原有的生产模式和技术手段已经不能满足经济的快速发展需求，全球面临结构转型升级问题，而人工智能、物联网、大数据、云平台等技术的发展，使得机器人成为了现代制造业的新生力量，机器人已成为当前*火热的研究和产业方向，是世界各主要国家的战略性发展方向[1]。例如，美国的再工业化[2]、欧盟的“工业4.0”[3]、日本复兴战略[4]、中国制造2025[5]等。 未来的世界是人机共处的世界。作为能够自主运动的机器，机器人为人类带来巨大便利的同时也带来了安全隐患，机器人故障引发的事故时有发生。1978年9月，日本广岛一间工厂的切割机器人将一名值班工人当作钢板切割造成惨案[6]；1989年，机器人棋手在与国际象棋冠军古德柯夫下棋时突然向金属棋盘释放出强电流，象棋大师被电身亡[7]；2013年，奥地利Roomba机器人受够了家庭琐事，而选择了“自焚”[8]；2014年1月，嫦娥三号玉兔月球车因机构控制出现故障而一度进入休眠[9]。机器人安全隐患成为机器人特别是人机交互机器人应用普及的巨大障碍。 造成上述问题的根源是传统的机器人测试用例与仿真用例受限，这意味着无论采取测试还是仿真来验证已有的设计都无法完全覆盖所有的测试与仿真路径。此时人们开始意识到传统的测试仿真等验证方法并不能满足安全攸关机器人的正确性、安全性验证要求。为了解决这些可靠性与安全性验证问题，2011年，美国国家科学基金会(National Science Foundation，NSF)提出未来重点支持与人协作机器人安全性与可靠性的研究工作，2013年，美国政府发布A Roadmap for U.S.Robotics的白皮书，提出未来五十年发展重点将从互联网转向机器人，并**次提出了将形式化方法应用于可靠性、安全性高的机器人应用领域。 形式化验证、机器证明的本质是用计算机推理取代人工推理，与传统的解析计算、分析和验证相比，更具逻辑性、完备性和准确性。目前，已有的形式化工具和机器证明平台中包含了实复数、矢量、空间、欧氏空间中微积分等[10.18]诸多内容，但这些内容还远远不能满足机器人安全验证的需求，特别是对连续、非线性、混杂系统的表征和应用还有很大距离。因此机器人相关理论的形式化建模与定理库构建已经成为形式化数学的一个迫切任务。 泛函变分的核心问题是求泛函的极值函数，极值函数的驻值条件是分析力学数学基础[19.21]。分析动力学作为经典物理学的基石之一提供普遍而统一的分析理论。它是变分理论的发源地和应用对象。动力学主要包括牛顿力学、拉格朗日力学和哈密顿力学三个体系。牛顿力学又称为矢量力学，解算时必须计及所有作用力的大小、方向及其作用点与质心的相对位置，因此很难建模复杂的动力学系统。拉格朗日力学[22.24]是对经典力学的一种的新的理论表述，着重于数学解析的方法，是分析力学中*重要的方法之一[25，26]。拉格朗日在其名著《分析力学》中把数学分析应用于质点和刚体力学，建立了拉格朗日方程，把力学体系的运动方程从以力为基本概念的牛顿形式，改变为以能量为基本概念的分析力学形式，奠定了分析力学的基础，为把力学理论推广应用到物理学其他领域(如振动、稳定性、刚体与刚体系统，以及机器人、天体与宇航器等领域)开辟了道路。拉格朗日力学是机器人动力学的基础理论力学之一。由于机器人机构的复杂性，一般主要采用齐次变换矩阵，根据机器人每个关节的位置、速度与描述速度转换的雅可比矩阵，建立机器人的动能、势能模型，从而根据拉格朗日力学的方程，构建机器人动力学的模型。然后分析动力学方程的解及其性质，*后通过工程实现成为动力学系统。 综上所述，变分理论与拉格朗日动力学理论是机器人的动力学的数学与力学基础，建立变分与拉格朗日动力学的形式化理论对机器人动力系统形式化建模与分析至关重要。本书以高阶逻辑形式化平台HOLLight[27]为工具，系统地对变分主要理论、拉格朗日力学主要理论以及机器人动力学理论进行形式化，弥补泛函与动力学形式化理论的空白。 1.2泛函变分、动力学与形式化验证 1.2.1泛函变分与动力学 泛函变分起源于1696年伯努利提出的*速降线问题，是数学分析的一个分支[28.33]。泛函变分的基本问题是关于泛函的极值问题，又称为变分问题或变分原理，其在物理学尤其是力学中有广泛的应用，如著名的虚功原理、动力学普遍方程、哈密顿原理等，是分析力学的数学分析基础。而且几乎所有的物理和力学的基本原理与运动方程都可以陈述为某一泛函变分的“变分法原理”，因此变分原理使许多重要的物理问题及技术问题得以解决。 动力学主要研究作用于物体的力与物体运动的关系[22.24]。自然界与工程中存在大量的动力学问题，动力学是物理学和天文学的基础，也是许多工程学科的基础。分析动力学作为经典物理学的基石之一提供普遍而统一的分析理论。它是很多数学理论的发源地和应用对象。人类近现代工业文明和对宇宙的认识都离不开动力学的发展。17世纪末，牛顿继承和发展前人的研究成果，提出力学运动的三条基本定律，使经典力学形成系统的理论。牛顿力学是矢量力学，具有数学形式简单和物理概念清晰等特点，在研究质点和简单刚体系统动力学问题方面取得了辉煌的成就，但在求解具有复杂约束系统和变形体的动力学问题方面则遇到了很大困难。这是因为在矢量力学方法中需要事先对系统中各质点的受力情况进行分析，而对于复杂约束系统，由于约束力的性质和分布在求解前是未知的使得求解过程变得极为复杂，也无法建立一般力学系统的动力学方程。 针对矢量力学遇到的困难，采用分析数学的方法来求解力学问题的理论在18世纪得到了迅速发展。分析动力学不仅有理论意义，也有着巨大的应用价值。它一方面提供了现代应用力学以及动力学一般理论*基本的原理和方法，另一方面也是振动、稳定性、刚体与刚体系统，以及机器人、天体与宇航器等领域的理论基础。1788年，拉格朗日撰写的《分析力学》是世界上*早的一本分析力学的著作，标志着拉格朗日力学理论体系的形成。拉格朗日力学采用能量和功来描述物体运动与相互作用之间的关系，通过达朗贝尔原理和虚位移原理建立了普遍形式下的动力学方程，为现代动力学理论的发展奠定了基础，也对近代数学和物理学的发展起到巨大的推动作用。其后几乎所有的分析力学的动力学方程都是从这个方程直接或间接导出的。 拉格朗日力学方法建立方程比较容易，但其求解规模很大。随着近代计算技术的发展，解决具有程式化特征的数学问题规模再大也能迎刃而解。因此在解决复杂动力学问题的计算机辅助分析软件中，均采用拉格朗日方程与加速度约束方程作为系统的动力学模型。许多数学工具软件都开发了动力学的仿真设计，如Maple[34]、Mathematica[35，36]和MATLAB[37，38]。这些软件主要采用数值计算和符号推理的方法来处理动力学的问题，很难处理具有复杂或非确定性的边界条件和初始条件的应用问题。而且，数值计算是采用近似处理的，结果存在不精确的问题，然而符号推理工具并不会严格要求用户检查表达式成立的前提条件，这样很容易忽略前提条件，从而导致错误发生[14]。虽然数值计算和符号推理的上述问题在一般情况下也许不会发生严重后果，但是对于一些安全攸关的重要应用领域，这些问题一旦发生，将带来灾难性的后果。更不幸的是，诸如测试和模拟等常规的验证方法很难发现设计中所存在的这类错误[39，40]。 1.2.2形式化数学 形式化数学是用计算机对数学理论进行形式化描述，对数学证明的正确性进行检查和验证，并且建立一个包含数学定义、定理和证明的形式化数学库[41]。Wiedijk[42]认为，数学发展历史上有三次革命：**次是公元前4世纪古希腊数学家欧几里得在《几何原本》中引入数学证明方法；第二次是19世纪柯西等人引入“严格”数学方法，以及费雷格的数理逻辑和康托尔的集合论；第三次就是当前正在进行的形式化数学。形式化数学不仅可以帮助数学家检查证明正确性从而构建更加可靠的数学理论，同时也是构建计算机可以理解的数学知识库，推动人工智能发展的重要基础，而且作为机器定理证明的基础，形式化数学也是计算机软硬件系统形式化验证的基础。 目前国际上适合数学形式化的主流的定理证明器都基于高阶逻辑和类型理论，包括英国剑桥大学开发的HOL4(HighOrderLogic)[43]、HOLLight[44]、Isabelle/HOL[45]，法国信息与自动化研究所开发的Coq[46]和美国NASA常用的PVS(PrototypeVerificationSystem)[47]。这些系统多数基于1972年开发的可计算函数逻辑(Logic of Computable Functions，LCF)证明检查器，理论基础来自LCF[48]。这些证明器基于极小的可信核心代码和公理系统的基本规则，扩展的代码和推理规则必须通过核心代码和规则的证明，这*大限度地保证了系统的可靠性[49]。 尽管形式化数学理论是一项艰巨的工作，但是通过全世界学者的共同努力，有一批非常有代表性的数学定理，甚至是困扰数学界已久的数学难题已由计算机完成证明，例如，四色定理、Brouwer不动点定理、Cauchy留数定理与Kepler猜想等[41，50，51]，这突显了数学理论形式化的重要性和可行性。这些难题的解决离不开定理证明系统对于基础数学理论的形式化工作，如集合论、抽象代数、概率论、矩阵代数、数学分析等。这些工作形成丰富的形式化数学定理库，为更进一步的数学形式化工作奠定非常重要的基础。 虽然目前形式化数学已经取得很大进展，但是工程数学的形式化成果还非常少。工程数学的模型构建和公式推导往往十分复杂，极易出错。在航空航天、核电控制、智能制造、列车控制和医疗器械等安全攸关系统中，微小错误可能导致灾难性后果。通过形式化技术建立系统的数学模型，进行严格的推导并验证正确性，是安全攸关系统正确构造和验证的*可靠的方法。因此形式化工程数学对提高工程领域的数学建模和推导能力有非常重要的作用。而泛函变分与动力学是工程领域的重要数学与力学基础，因此本书基于已有的形式化数学工作，对泛函变分与拉格朗日力学的主要理论进行形式化，且在此基础之上对机器人动力学内容进行形式化，填补泛函与动力学形式化理论的空白，为机器人的形式化验证奠定基础。 本书工作是在高阶逻辑定理证明器HOLLight系统上开展的，在2.4节有关于HOLLight的详细介绍。 1.2.3形式化验证 在计算机科学和软件工程领域，形式化方法是基于数学的特种技术，适合于软件和硬件系统的描述、开发和验证。形式化方法使用严格的数学分析以提高软件和硬件设计的正确性和可靠性。采用形式化方法的成本较高，通常用于开发注重安全性的系统。 机器人作为安全攸关系统主要源于其运动性，因此关于机器人运动的安全性和正确性形式化验证方法成为研究的焦点。近年来形式化验证已被用来帮助开发复杂的机器人系统[52]。德国不莱梅大学的T.ubig[53]等用定理证明方法对自动小车避障及路径规划算法进行验证，并给出改进意见，使得算法的安全性能显著提升。卡内基梅隆大学的Mitsch[54]等采用混杂系统模型和定理证明建模和验证移动机器人的运动和避障安全属性。 美国国防高级研究计划局(Defense AdvancedResearch Projects Agency，DARPA)启动了HACMS项目[55]，即“高可信军事网络系统”（High-Assurance Cyber Military Systems)，开发的主要是形式化验证技术，其目标就是让黑客难以入侵到诸如无人机等军事指挥控制网络系统中。这项技术在“小鸟”无人军事直升机进行了公开测试，参与测试的黑客们努力了六周却始终无法入侵该系统，有力地证明了形式化技术的可靠性。 机器人控制、列车控制、飞行控制、核