Page 40 - 《软件学报》2025年第8期

张善强 等: 单球驱动平衡机器人运动学和动力学形式化验证 3463

的优势在于, 利用球体作为驱动轮, 对地形的变化具有较强的适应性. 在运动时能够在受空间限制的环境中实现转
向、小半径转弯以及原地进行任意方向的移动, 在运输 [1] 、搜救 [2] 、医疗服务 [3] 等领域都具有广阔的应用前景.
未来的世界将迎来人机共处的新时代, 机器人的普及为人类带来了巨大的便利. 然而, 随着机器人具备了自主
运动能力, 与之相关的安全隐患也日益凸显. 机器人故障可能影响效率或引发事故. 2014 年 1 月, 嫦娥三号玉兔月
球车因机构控制出现故障而一度进入休眠 [4] . 2016 年 11 月, 在第 18 届中国国际高新技术成果交易会上, 一台服务
机器人在无外部指令的情况下突发故障, 冲撞展台并损坏玻璃结构, 导致部分设备受损, 并造成现场人员受伤 [5] .
2024 年 1 月, 美国得克萨斯州某超级工厂发生机器人相关事故, 一名工程师在维修过程中遭机械臂抓伤 [6] .
机器人安全隐患已经成为机器人技术普及的重要阻碍, 特别是在人机交互机器人中. 因此, 在执行各项任务时
的单球驱动平衡机器人将面临一个至关重要的问题. 以货物运输为例, 机器人是否能够准时且准确地沿指定路线
到达目的地. 在人机互动的场景中, 如何有效避免碰撞和倾倒, 确保人员安全, 显得尤为关键. 鉴于此, 深入研究单
球驱动平衡机器人的运动学和动力学问题, 不仅会提高其运动性能, 更有利于确保其运动的正确性与安全性.
对单球驱动平衡机器人的运动学和动力学建模和分析时, 传统方法主要包括纸笔演算、数值计算和计算机代
数系统. 由于在运动学和动力学分析的过程中, 涉及等式代换和求导等复杂运算, 纸笔演算的方法耗时费力, 容易
引入人为错误; 计算机数值计算方法指利用计算机软件进行数值计算, 这只能给出待解问题的数值解, 但无法揭示
问题的内在逻辑和根本原理, 这对于安全攸关的机器人系统, 显然是不够的; 计算机代数系统比如 Mathematica 能
够高效进行符号代数运算, 但是系统的核心包含未经验证的符号算法 [7] , 可能为机器人运动学和动力学模型分析
引入缺陷. 运动学和动力学的研究对于单球驱动平衡机器人的安全性和正确性十分重要, 仅依赖这些传统技术手

段可能会带来灾难性后果.
定理证明的形式化方法 [8] 克服了传统方法的局限性, 它使用数学逻辑描述系统及其性质, 借助相应的数学知
识对系统设计的性质进行形式化推导. 使用定理证明的方法对机器人运动学和动力学进行建模和分析, 避免了纸
笔证明、计算机数值模拟和计算机符号计算的局限性. 进而, 机器人系统的安全性和可靠性获得了强有力的保障.
因此, 采用定理证明的形式化方法对单球驱动平衡机器人运动学和动力学模型进行分析和验证, 可以保证系统的
正确性和完备性.
本文使用高阶逻辑定理证明器 HOL Light 对单球驱动平衡机器人的运动学和动力学模型进行形式化验证, 主
要贡献如下.
(1) 形式化建模和验证单球驱动平衡机器人正向运动学模型.
(2) 形式化建模和验证单球驱动平衡机器人机身和球轮的速度模型.
(3) 形式化建模和推导单球驱动平衡机器人拉格朗日动力学模型.
本文第 1 节介绍单球驱动平衡机器人运动学动力学形式化验证的相关工作. 第 2 节介绍 HOL Light 定理证明
器和单球驱动平衡机器人. 第 3 节介绍单球驱动平衡机器人运动学及其形式化建模和验证. 在第 3 节对单球驱动
平衡机器人末端速度形式化验证的基础上, 第 4 节进一步通过拉格朗日方程法分析单球驱动平衡机器人的动力
学, 并对其拉格朗日动力学方程进行高阶逻辑建模和推导. 第 5 节总结全文.

1 相关工作

为使读者更清晰地了解单球驱动平衡机器人的发展历程, 且鉴于现有研究尚未涉及其运动学和动力学的形式
化验证, 本文的相关工作将首先介绍该机器人的研究现状, 并探讨定理证明方法在其他类型机器人中的应用, 为本
研究工作的进一步开展奠定基础.

1.1 单球驱动平衡机器人研究现状
近年来, 单球驱动平衡机器人领域的研究取得了丰硕的成果. Lauwers 等人 [9] 把该型机器人简化为一个倒立摆
模型, 并使用拉格朗日方程法对其动力学进行建模. Satici 等人 [10] 分析了单球驱动平衡机器人的运动学以及应用