摘要
单球驱动平衡机器人是一种具有全向运动性的机器人,其灵活性能在狭小或复杂环境中得到充分体现,因此受到广泛关注.在该型机器人运动学和动力学设计过程中,保证其模型的正确性至关重要.基于测试和仿真的传统方法难以穷尽系统所有状态,因此可能无法捕捉到某些设计缺陷或潜在的安全风险.为确保单球驱动平衡机器人满足安全攸关机器人的正确性、安全性验证要求,在定理证明器HOL Light中,基于实分析库、矩阵分析库、机器人运动学和动力学库等定理证明库,构建单球驱动平衡机器人运动学和动力学的形式化模型,并进行高阶逻辑推导与证明.
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.
作者
张善强
张景芝
施智平
王国辉
关永
ZHANG Shan-Qiang;ZHANG Jing-Zhi;SHI Zhi-Ping;WANG Guo-Hui;GUAN Yong(Information Engineering College,Capital Normal University,Beijing 100048,China;Beijing Key Laboratory of Electronic System Reliability Technology(Capital Normal University),Beijing 100048,China;Beijing Key Laboratory of Light Industrial Robots and Safety Verification(Capital Normal University),Beijing 100048,China)
出处
《软件学报》
北大核心
2025年第8期3462-3476,共15页
Journal of Software
基金
国家自然科学基金(62272323,62272322,62372312)。
