Page 44 - 《软件学报》2025年第8期
P. 44
张善强 等: 单球驱动平衡机器人运动学和动力学形式化验证 3467
系 T 分别在球轮和机身的质心, l 是机身质心与球轮质心的距离 [30] .
对于单球驱动平衡机器人而言, 其运动学研究涵盖了正向运动学、空间速度及末端速度. 在对单球驱动平衡
机器人的正向运动学分析中, 通过坐标系 B 相对于惯性系 S 的齐次矩阵 g sb 和坐标系 T 相对于坐标系 B 的齐次矩
阵 g bt 的乘积来确定末端位姿 g st . 此外, 该机器人的空间速度 ˆ V bt 可通过计算位姿矩阵的导数 ˙ g bt 与位姿矩阵的逆矩
阵 g −1 的乘积得到. 最后, 在确定了末端位姿和空间速度的基础上, 可以进一步确定机器人的末端速度 ˙ p st .
bt
T
l B
S
图 2 单球驱动平衡机器人模型图
3.2 正向运动学形式化验证
末端位姿, 即坐标系 T 相对于惯性系 S 的位姿, 由坐标系 B 相对于惯性系 S 的位姿和坐标系 T 相对于坐标
系 B 的位姿通过矩阵相乘得到. 由公式 (1) 得, 如下:
R sb p sb R bt lR bt e 3 R sb R bt R sb lR bt e 3 + p sb R st R sb lR bt e 3 + p sb
g st = g sb g bt = = = (4)
0 1 0 1 0 1 0 1
其中, g st 表示坐标系 T 相对于惯性系 S 的位姿, g sb 表示坐标系 B 相对于惯性系 S 的位姿, g bt 表示坐标系 T 相对
于坐标系 B 的位姿, R st 表示坐标系 T 相对于惯性系 S 的旋转矩阵, R sb 表示坐标系 B 相对于惯性系 S 的旋转矩阵,
R bt 表示坐标系 T 相对于坐标系 B 的旋转矩阵, p sb 表示坐标系 B 相对于惯性系 S 的位置向量, e 3 表示单位向量
T
[0,0,1] . 对公式 (4) 进行形式化描述如定理 1 所示.
定理 1. 末端位姿.
!gsb gbt gst pbt Rst psb pst Rbt Rsb t l.
[A1] : gsb = (\t.homo_trans(psb t)(Rsb t))/\
[A2] : gbt = (\t.homo_trans(pbt t)(Rbt t))/\
[A3] : pbt = (\t.l%%(Rbt t)∗∗(basis 3))/\
[A4] : Rst = (\t.(Rsb t)∗∗(Rbt t))/\
[A5] : gst = (\t.gsb(t)∗∗gbt(t))
[G1] : ==> gst = (\t.homo_trans(psb t +Rsb t ∗∗l%%Rbt t ∗∗basis 3)(Rstt)),
其 中 , homo_trans 表 示 给 定 位 置 向 量 和 旋 转 矩 阵 返 回 对 应 的 齐 次 变 换 矩 阵 ; 条 件 A 1 和 条 件 A 2 分 别 是
[ ] [ ]
R sb p sb R bt p bt
g sb = 和 g bt = 的形式化表示; \t 表示函数的自变量为 t; 条件 A3 是 p bt = lR bt e 3 的形式化表
0 1 0 1
[ ]
示; 条件 A4 和条件 A5 分别是 R st = R sb R bt 和 g st = g sb g bt 的形式化表示; 目标 G1 是 g st = R st R sb lR bt e 3 + p sb 的形
0 1
式化表示.
定理 1 的证明首先通过采用 SIMP_TAC 策略将条件 A5 代入到目标 G1 中, 其次将条件 A1–A4 代入到当前
目标, 随后应用矩阵乘法定理进行重写, 以此完成该定理的证明.
在定理证明的过程中, 是以目标为导向的, 所有的条件都是为了服务最终的证明目标, 直到该目标被证明完
p 虽然常以简单的符号形式出现, 但这些符号实际
成. 在数学表示和计算中, 齐次矩阵 g、旋转矩阵 R 和位置向量
上代表了更为具体的数学对象或函数. 在形式化的数学表示中, 这些矩阵和向量的函数属性被明确表示出来, 从而
保证了形式化证明的严谨性和正确性.
形式化验证过程通常要求扎实的数学理论基础, 不仅需要明确每个变量的类型, 还需在推理过程中灵活应用
