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

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

多种策略和定理, 这些都使得形式化验证成为一项颇具挑战的任务.

3.3 空间速度形式化验证
在运动过程中, 单球驱动平衡机器人展现出了包括旋转和平移的复合运动特性, 因此, 这种机器人的速度是由
ˆ V bt , 即坐标系 相对于坐标系 的速度, 由坐标系 相对于坐标系
其旋转速度和平移速度共同构成的. 空间速度 T B T
B 的位姿的导数 ˙ g bt 和其逆 g −1 的乘积表示, 由公式 (2) 得, 具体计算过程如下.
bt

([ ])[ ] [ ][ ] [ ]
d R T R T 0
−1
ˆ V bt = ˙g bt g = R bt lR bt e 3 bt −le 3 = ˆ ω bt R bt l ˆω bt R bt e 3 bt −le 3 = ˆ ω bt (5)
bt dt 0 1 0 1 0 0 0 1 0 0
其中, R T 表示坐标系 T 相对于坐标系 B 的旋转矩阵的转置, ω bt 表示坐标系 T 相对于坐标系 B 的角速度, ˆ ω bt 表示
bt
ω bt 的反对称矩阵 [30] . 公式 (5) 通过矩阵求导、矩阵求逆和矩阵相乘得到坐标系 T 相对于坐标系 B 的线速度为 0.
对公式 (5) 进行形式化描述如定理 2 所示.
定理 2. 空间速度.
!gbt Rbt Rbt' t l.
[A1] : (!t.rotation_matrix(Rbt t))/\
[A2] : (Rbt has_v1matrix_derivative(Rbt t))(at t)/\
′
[A3] : gbt = (\t.homo_trans((l%%(Rbt t))∗∗(basis 3))(Rbt t))/\
[G1] : ==> spatial_velocity gbt UNIV t =

∧
twist_wedge(pastecart(vec 0 : real 3)(matrix3_vee(spatial_velocity Rbt UNIV t))),
其中, spatial_velocity 表示给定位姿矩阵返回该位姿矩阵的导数和逆的乘积, twist_wedge 表示线速度和角速度的
组合, pastecart 表示两个向量的拼接, matrix3_vee 表示给定反对称矩阵返回对应的向量. 条件 A1 是 R bt 是旋转矩
[ ]
阵的形式化表示; 条件 A2 是旋转矩阵 R bt 有导函数 ˙ R bt 的形式化表示; 条件 A3 是 g bt = R bt lR bt e 3 的形式化表
0 1
[ ]
0
ˆ ω bt
示; 目标 G1 是 ˙ g bt g = 的形式化表示.
−1
bt 0 0
定理 2 的证明通过采用 REWRITE_TAC 策略, 将空间速度重写为对应齐次矩阵的导数与其逆矩阵乘积的形
( ([ ])
d R bt lR bt e 3
式 ( ˆ V bt = ˙g bt g ). 接着, 证明过程分为两个子目标, 一是证明齐次矩阵求导后的表达式成立 =
−1
bt dt 0 1
[ ])
ˆ ω bt R bt l ˆω bt R bt e 3 [30]
, 在此过程中, 证明 ˙ R bt = ˆω bt R bt 这一等式, 对齐次矩阵导数的表达式进行代换; 二是证明其
0 0
[ ] −1 [ ]
 R bt R T 
 lR bt e 3 bt −le 3 

求逆后的表达式成立    = . 最终, 结合 SIMP_TAC 策略应用正交矩阵的定义以及齐
0 1 0 1

次零矩阵和齐次矩阵乘法定理, 完成整个证明过程.

3.4 末端速度形式化验证
在应用拉格朗日方程法进行动力学分析过程中, 首先需求解系统的动能和势能, 其中动能包括机身和球轮的
动能. 为此, 关键在于确定机身相对于惯性系的速度, 亦即末端速度. 具体计算过程如下所示.

①
˙ p st = v st +ω st × p st
②
= v sb + p sb ×R sb ω bt +ω st × p st
③
= ˙p sb −ω sb × p sb + p sb ×R sb ω bt +ω sb × p st +R sb ω bt × p st
= ˙p sb +ω st ×(p st − p sb ) ④
⑤
= ˙p sb +ω st × p bt
⑥ (6)
= ˙p sb +lω st ×R st e 3
其中, p st 是坐标系 T 相对于惯性系 S 的位置向量, ˙ p st 表示坐标系 T 相对于惯性系 S 的速度, ˙ p sb 表示坐标系 B 相
对于惯性系 S 的速度, v st 表示坐标系 T 相对于惯性系 S 的线速度, “ × ”表示向量的叉乘. ① 由上述相对速度 v st =
T [30] ˆ xy = x×y 运算法则得到; ①到②则根据公式 (2) 和公式
− ˙ R st R p st + ˙p st 结合 ˙ R st = ˆω st R st 这一等式以及 (5) 得,
st