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

软件学报 ISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac.cn
2025,36(8):3462−3476 [doi: 10.13328/j.cnki.jos.007345] [CSTR: 32375.14.jos.007345] http://www.jos.org.cn
©中国科学院软件研究所版权所有. Tel: +86-10-62562563

*
单球驱动平衡机器人运动学和动力学形式化验证

张善强 1 , 张景芝 1 , 施智平 1,2 , 王国辉 1,2 , 关 永 1,3

1
(首都师范大学 信息工程学院, 北京 100048)
2
(电子系统可靠性技术北京市重点实验室 (首都师范大学), 北京 100048)
3
(轻型工业机器人与安全验证北京市重点实验室 (首都师范大学), 北京 100048)
通信作者: 张景芝, E-mail: 6835@cnu.edu.cn

摘 要: 单球驱动平衡机器人是一种具有全向运动性的机器人, 其灵活性能在狭小或复杂环境中得到充分体现, 因
此受到广泛关注. 在该型机器人运动学和动力学设计过程中, 保证其模型的正确性至关重要. 基于测试和仿真的传
统方法难以穷尽系统所有状态, 因此可能无法捕捉到某些设计缺陷或潜在的安全风险. 为确保单球驱动平衡机器
人满足安全攸关机器人的正确性、安全性验证要求, 在定理证明器 HOL Light 中, 基于实分析库、矩阵分析库、
机器人运动学和动力学库等定理证明库, 构建单球驱动平衡机器人运动学和动力学的形式化模型, 并进行高阶逻
辑推导与证明.
关键词: 单球驱动平衡机器人; 运动学和动力学; 形式化验证; 定理证明; HOL Light
中图法分类号: TP311

中文引用格式: 张善强, 张景芝, 施智平, 王国辉, 关永. 单球驱动平衡机器人运动学和动力学形式化验证. 软件学报, 2025, 36(8):
3462–3476. http://www.jos.org.cn/1000-9825/7345.htm
英文引用格式: Zhang SQ, Zhang JZ, Shi ZP, Wang GH, Guan Y. Formal Verification of Kinematics and Dynamics of Single-sphere
Driven Balancing Robot. Ruan Jian Xue Bao/Journal of Software, 2025, 36(8): 3462–3476 (in Chinese). http://www.jos.org.cn/1000-
9825/7345.htm

Formal Verification of Kinematics and Dynamics of Single-sphere Driven Balancing Robot
1
1
1,2
1,2
ZHANG Shan-Qiang , ZHANG Jing-Zhi , SHI Zhi-Ping , WANG Guo-Hui , GUAN Yong 1,3
1
(Information Engineering College, Capital Normal University, Beijing 100048, China)
2
(Beijing Key Laboratory of Electronic System Reliability Technology (Capital Normal University), Beijing 100048, China)
3
(Beijing Key Laboratory of Light Industrial Robots and Safety Verification (Capital Normal University), Beijing 100048, China)
Abstract: The single-sphere driven balancing robot is an omnidirectional mobile robot, whose flexibility is particularly evident in narrow
or complex environments. During the design of the kinematics and dynamics for this type of robot, it is crucial to ensure the correctness
of the model. Traditional methods based on testing and simulation may not cover all system states and thus might fail to identify certain
design flaws or potential safety risks. To ensure that the single-sphere driven balancing robot satisfies the correctness and safety
verification requirements for safety-critical robots, a formal model of its kinematics and dynamics is constructed using the HOL Light
theorem prover. The model is based on theorem libraries such as the real analysis library, matrix analysis library, and robot kinematics and
dynamics library, and involves higher-order logic derivation and proof.
Key words: single-sphere driven balance robot; kinematics and dynamics; formal verification; theorem proving; HOL Light
单球驱动平衡机器人主要由球轮、驱动系统、机身 3 大部件组成, 该型机器人利用驱动滚轮与底部支撑球体
之间的摩擦产生驱动力, 实现机器人的自平衡、自旋以及全方位移动 [1] . 此类机器人相较于其他轮式机器人最大

* 基金项目: 国家自然科学基金 (62272323, 62272322, 62372312)
本文由“形式化方法与应用”专题特约编辑陈明帅研究员、田聪教授、熊英飞副教授推荐.
收稿时间: 2024-08-24; 修改时间: 2024-10-14; 采用时间: 2024-11-26; jos 在线出版时间: 2024-12-10
CNKI 网络首发时间: 2025-04-17