| 本文已被：浏览 1479次 下载 1750次 |
码上扫一扫！ |
|
|
| 单球驱动平衡机器人运动学和动力学形式化验证 |
|
张善强1, 张景芝1, 施智平1,2, 王国辉1,2, 关永1,3
|
|
1.首都师范大学 信息工程学院, 北京 100048;2.电子系统可靠性技术北京市重点实验室 (首都师范大学), 北京 100048;3.轻型工业机器人与安全验证北京市重点实验室 (首都师范大学), 北京 100048
|
|
| 摘要: |
| 单球驱动平衡机器人是一种具有全向运动性的机器人, 其灵活性能在狭小或复杂环境中得到充分体现, 因此受到广泛关注. 在该型机器人运动学和动力学设计过程中, 保证其模型的正确性至关重要. 基于测试和仿真的传统方法难以穷尽系统所有状态, 因此可能无法捕捉到某些设计缺陷或潜在的安全风险. 为确保单球驱动平衡机器人满足安全攸关机器人的正确性、安全性验证要求, 在定理证明器HOL Light中, 基于实分析库、矩阵分析库、机器人运动学和动力学库等定理证明库, 构建单球驱动平衡机器人运动学和动力学的形式化模型, 并进行高阶逻辑推导与证明. |
| 关键词: 单球驱动平衡机器人 运动学和动力学 形式化验证 定理证明 HOL Light |
| DOI：10.13328/j.cnki.jos.007345 |
| 分类号: |
| 基金项目:国家自然科学基金(62272323, 62272322, 62372312) |
|
| Formal Verification of Kinematics and Dynamics of Single-sphere Driven Balancing Robot |
|
ZHANG Shan-Qiang1, ZHANG Jing-Zhi1, SHI Zhi-Ping1,2, WANG Guo-Hui1,2, GUAN Yong1,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 |
