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

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

库. 这些定理库为本文的工作提供了基础支持. 因此, 本文选择使用 HOL Light 定理证明器对单球驱动平衡机器人
运动学和动力学进行形式化验证. 为了方便对其他部分的理解, 这里对 HOL Light 定理证明器中一些常用的符号
和函数进行说明, 如表 1 所示.

表 1 HOL Light 中的符号与函数

HOL Light符号 标准符号 含义
/\ 与 逻辑与
==> ⇒ 推出
−− − 负号
! ∀ 对所有的
? ∃ 存在
\ lambda 定义函数
&x x 从自然数到实数的类型转换
v$i v i 向量 v 的第 i 个分量
A∗∗B AB 矩阵乘
c%v cv 向量标量乘
c%%A cA 矩阵标量乘
xcrossy x×y 向量的外积
vec0 − → 零向量
0
basis3 e 3 单位向量 [0,0,1] T
matrix_invA A −1 矩阵 A 的逆
x IN S x ∈ S x属于集合 S

2.2 单球驱动平衡机器人
单球驱动平衡机器人主要构成包括 3 个核心部分, 分别是球轮、驱动系统以及机器人的机身. 一般情况下, 机
身与驱动系统设计为一体, 机身部分整合了驱动系统 (包括电机和驱动滚轮) 及其他关键组件, 如电池和惯性测量
单元等 [9] .
单球驱动平衡机器人的驱动系统由电机驱动、驱动皮带和驱动滚轮等组成. 这些驱动滚轮紧贴在球体的赤道
线上 [28] . 驱动滚轮通过驱动皮带与电机相连, 借助于驱动滚轮与球体之间的摩擦力驱动球体移动. 如图 1 所示. 偏
航轴承是一种旋转轴承, 主要用于控制机身的旋转. 编码器作为关键的反馈传感器, 用于精确测量机器人的位置和
运动. 编码器能够准确检测旋转角度和直线位移, 为机器人的精确运动提供数据支持. 皮带张紧器则用于调节皮带
的松紧度.

偏航轴承
电机驱动
编码器 皮带张紧器
驱动皮带 球张紧器
驱动滚轮 球

图 1 驱动系统

单球驱动平衡机器人是一种典型的欠驱动系统, 欠驱动系统是指独立控制输入的维数少于系统自由度的系
统, 本质上属于非线性系统. 通过减少驱动器数量, 不仅可以简化设计, 提高系统的灵活性, 还能够有效降低成本,
减少系统的重量和体积, 并降低能耗. 在实际工程应用中, 使用少于标准数量的执行器来实现系统控制是一项具有
挑战性的尝试. 欠驱动系统作为一种特殊的非线性系统, 其研究有助于深化对一般非线性系统的控制问题的理解.