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

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

∧
M = vector[vector[Ib;&0] : real 2;vector[&0;It] : real 2] : real 2 2/\
∧ ∧
∧
[A7]: f = (\t : real 1.(vector[lift(&0);lift(tau)] : real 1 2))/\
∧
∧ ∧
rr = (\u : real (2,1)finite_sum.(vector[lift(fstcart u$1);lift(fstcart u$2)] : real 1 2))/\
∧ ∧
∧
[A8]: lagrange_equations_autonomous s s0 s1 ke ue q f rr t
[G1]: ==> M ∗∗(q t) = vector[&0;tau].
′′
条件 A3 表示广义坐标 q 由 φ 和 组成, 广义速度 ˙ q 由 ˙ φ 和 组成以及广义速度的导数 ¨ q 由 ¨ φ 和 组成; 条件
˙ δ
δ
¨ δ
A4 表示广义坐标 φ 的导函数为 , ˙ δ, 广义速度 ˙ φ 的导函数为 , ˙ ¨ δ.
¨ φ δ 的导函数为
˙ φ δ 的导函数为
定理 5 的条件和证明和定理 4 类似, 在此不再一一赘述. 以上通过对单球驱动平衡机器人 XOZ 面和 XOY 面
的拉格朗日动力学方程进行高阶逻辑建模和推导, 保证了该型机器人动力学模型的正确性, 提高了机器人的可靠
性和安全性.

5 总 结
本文通过使用 HOL Light 定理证明器, 形式化建模并验证了单球驱动平衡机器人的运动学和动力学高阶逻辑
模型. 在运动学部分, 本文对单球驱动平衡机器人的正向运动学、空间速度以及末端速度进行形式化建模和验证.
在此基础上, 进一步对单球驱动平衡机器人 XOZ 面的拉格朗日动力学方程进行形式化建模和验证. 为了提升控制
的精确度, 本文还构建并验证了 XOY 面的拉格朗日动力学方程. 形式化验证方法克服了传统验证方法的局限, 保
障了设计的正确性与安全性. 值得一提的是, 在对 XOZ 面的动力学方程验证过程中, 发现并纠正了两处系数错误.
这不仅有助于提高系统的正确性和安全性, 也增强了验证工作者的信心. 这项工作不仅保证了单球驱动平衡机器
人运动学和动力学模型的正确性, 并对未来机器人控制设计与实现提供了可靠性和安全性保障.
另外, 本文验证的文献 [10] 还通过部分反馈线性化和函数设计, 提出能量整形控制方法, 并推导了相应的控
制方程. 与此同时, 文章还基于 Lyapunov 稳定性理论, 对该控制系统进行了数学推导和分析. 鉴于现有的控制相关
定理库尚不完善, 作者计划在未来的研究中致力于进一步完善这一定理库, 并对所推导的控制方程进行形式化验证.

References:
[1] Kumagai M, Ochiai T. Development of a robot balancing on a ball. In: Proc. of the 2008 Int’l Conf. on Control, Automation and Systems.
Seoul: IEEE, 2008. 433–438. [doi: 10.1109/ICCAS.2008.4694680]
[2] Tsai CC, Chan CK, Kuo LC. LQR motion control of a ball-riding robot. In: Proc. of the 2012 IEEE/ASME Int’l Conf. on Advanced
Intelligent Mechatronics. Kaohsiung: IEEE, 2012. 861–866. [doi: 10.1109/AIM.2012.6265988]
[3] Shomin M, Forlizzi J, Hollis R. Sit-to-stand assistance with a balancing mobile robot. In: Proc. of the 2015 IEEE Int’l Conf. on Robotics
and Automation. Seattle: IEEE, 2015. 3795–3800. [doi: 10.1109/ICRA.2015.7139727]
[4] Liu FC, Liu L, Li Q, Qin L, Wang WK. Literature review of effects of gravity on motion behavior of space mechanisms. Manned
Spaceflight, 2017, 23(6): 790–797 (in Chinese with English abstract). [doi: 10.16329/j.cnki.zrht.2017.06.013]
[5] Li ZQ. Reflection on the theory of legal liability in the age of artificial intelligence——Intelligent robot as a pointcut. Journal of Dalian
University of Technology (Social Sciences), 2019, 40(5): 78–87 (in Chinese with English abstract). [doi: 10.19525/j.issn1008-407x.2019.
05.010]
[6] Liu YM. Where is the safety risk of “robot wounding”. Grand Garden of Science, 2024, (2): 62–63 [doi: 10.3969/j.issn.1003-1871.2024.
02.025]
[7] Durán AJ, Pérez M, Varona JL. Misfortunes of a mathematicians’ trio using computer algebra systems: Can we trust? arXiv:1312.3270,
2023.
[8] Hasan O, Tahar S. Formal verification methods. In: Mehdi Khosrow-Pour DBA, ed. Encyclopedia of Information Science and
Technology. 3rd ed., Hershey: Information Science Reference, 2015. 7162–7170. [doi: 10.4018/978-1-4666-5888-2.ch705]
[9] Lauwers TB, Kantor GA, Hollis RL. A dynamically stable single-wheeled mobile robot with inverse mouse-ball drive. In: Proc. of the
2006 IEEE Int’l Conf. on Robotics and Automation. Orlando: IEEE, 2006. 2884–2889. [doi: 10.1109/ROBOT.2006.1642139]
[10] Satici AC, Donaire A, Siciliano B. Intrinsic dynamics and total energy-shaping control of the ballbot system. Int’l Journal of Control,
2017, 90(12): 2734–2747. [doi: 10.1080/00207179.2016.1264630]