软件学报

作者：张善强，张景芝，施智平，王国辉，关永

单位：张善强，首都师范大学 信息工程学院, 北京 10004811,张景芝，首都师范大学 信息工程学院, 北京 10004802,施智平，首都师范大学 信息工程学院, 北京 100048;电子系统可靠性技术北京市重点实验室 (首都师范大学), 北京 10004803,王国辉，首都师范大学 信息工程学院, 北京 100048;电子系统可靠性技术北京市重点实验室 (首都师范大学), 北京 10004804,关永，首都师范大学 信息工程学院, 北京 100048;轻型工业机器人与安全验证北京市重点实验室 (首都师范大学), 北京 10004805

关键词：单球驱动平衡机器人;运动学和动力学;形式化验证;定理证明;HOL Light

基金：国家自然科学基金(62272323, 62272322, 62372312)

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

来源：2025年第8期

《软件学报》期刊编辑部

查看软件学报杂志2025年第8期