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

3464 软件学报 2025 年第 36 卷第 8 期

拉格朗日方程法对 XOZ 面进行动力学建模. Kumagai 等人 [1] 对单球驱动平衡机器人进行了改进, 通过 3 个全向轮
与底部支撑球体的摩擦产生驱动力, 控制平衡、自旋以及全方位移动, 使其运动更加稳定. 之后, Fankhauser 等人 [11]
基于全三维动力学模型, 使得该型机器人不仅在球体上保持了动态平衡, 还显著提升了灵活性和运动能力. 为使该
型机器人的方向控制更加容易, You 等人 [12] 利用麦克纳姆轮的全向特性, 设计出了一种麦克纳姆轮驱动的单球驱
动平衡机器人.
上述单球驱动平衡机器人的研究现状有助于加深对该型机器人的理解, 为进一步分析其运动学和动力学, 并
进行后续验证提供了基础. 本文验证的是 Satici 等人 [10] 的工作, 对该机器人的运动学和 XOZ 面的动力学方程进行
形式化验证. 在此基础上, 为了提高控制的稳定性, 本文还构建并验证了 XOY 面的动力学方程.

1.2 定理证明方法在机器人运动学和动力学领域的应用
在现代机器人系统的研究与应用中, 运动学和动力学的正确性对于确保系统的安全至关重要. 比如, 在高危行
业如核设施管理中, 自动化搬运机器人系统对安全性和可靠性的需求极为严格. 这些机器人负责处理和运输放射
性或危险物质, 任何系统故障都可能威胁人员安全并造成环境风险. 近年来, 形式化验证已成为开发这些安全攸关
型机器人系统的一个关键方法, 以确保它们的功能安全与操作可靠性 [13] . 这种方法不仅提高了机器人系统的整体
性能, 也显著提升了它们在关键应用中的安全标准.
在机器人运动学领域, Farooq 等人 [14] 在 HOL Light 定理证明器中, 应用 HOL Light 的几何理论对双连杆平面
机械手运动学进行形式化分析, 并将其用于分析二维仿人步行机器人; Affeldt 等人 [15] 在 Coq 定理证明器 [16] 中形
式化了反对称矩阵和四元数的指数等理论, 并对等距同构、齐次表示、DH 标定等刚体变换的表示进行了形式化,
在此基础上, 实现了串联机器人运动学模型的构建与验证; Wu 等人 [17] 在 HOL4 中建立旋量理论, 结合 HOL4 中的
几何理论, 形式化分析了六自由度串联机器人的运动学; 陈琦等人 [18] 在 HOL Light 定理证明器中形式化描述平面
并联机构的相关数学理论, 建立正向运动学的高阶逻辑模型, 验证正向运动学的一般性求解算法, 从而确保了平面
并联机构运动学分析的正确性和分析求解方法的可靠性; 谢果君等人 [19] 在 Coq 定理证明器中对 DH 坐标系进行
形式化建模, 构建了机械臂正向运动学的形式化定义, 并对机械臂运动的可分解性进行了形式化验证, 还对工业机
器人中常见的连杆结构及机器人进行形式化建模, 并完成了正向运动学的形式化验证.
在机器人动力学领域, Abed 等人 [20] 在 HOL Light 定理证明器中, 对导航和飞机等的坐标框架进行形式化, 确
保了飞机的正确方向和位置, 并形式化无人机的连续动力学, 最后, 对无人机进行形式化稳定性分析; Rashid 等人 [21]
使用高阶定理证明器 HOL Light, 通过对注射器、相机和平台等部件的形式化建模以及它们之间相互关系的形式
化验证, 并实现注射器移动的形式化, 进而对细胞注射机器人动力学分析进行了形式化验证.
另外, 张景芝 [22] 在其博士论文中, 对齐次矩阵、齐次向量、矩阵值函数的微分、空间速度、矩阵伴随变换等
机器人运动学基础进行了形式化定义以及相关定理的形式化证明. 除此之外, Zhang 等人 [23] 在 HOL Light 定理证
明器中实现了泛函变分理论的形式化验证. 在此基础上, Guan 等人 [24] 在 HOL Light 定理证明器中建立拉格朗日力
学的形式化定理库, 为拉格朗日力学的应用奠定了必要的基础. 基于以上相关工作, 本文使用定理证明器 HOL
Light 对单球驱动平衡机器人运动学和动力学进行形式化验证.

2 基础知识

2.1 HOL Light 定理证明器
HOL Light [25] 是国际上最著名的交互式定理证明器之一, 它采用了 OCaml 语言 (一个强类型函数式编程语言
ML 的衍生变体) 作为其定理证明的编程基础 [26] . HOL Light 的理论框架由类型、常数、定义以及定理构成, 新的
定理则是通过应用基本公理、原始推理规则以及之前验证过的定理和推理规则得出的 [27] . 在 HOL Light 中, 证明
一个目标通常遵循形式 A1,A2,...,An ==> G, 其中 A1,A2,...,An 代表一系列假设或前提条件, 而 G 是需要被证
明的结论. 定理的证明过程涉及策略的反复使用和已知定理的应用, 直至与已知条件相匹配, 从而实现定理证明的目标.
目前, 在 HOL Light 定理证明器中存在实分析库、矩阵分析库、机器人运动学库和机器人动力学库等定理