Formal Verification of Kinematics and Dynamics of Single-sphere Driven Balancing Robot
Author:
Affiliation:

Clc Number:

TP311

  • Article
  • | |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • | |
  • Comments
    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.

    Reference
    Related
    Cited by
Get Citation

张善强,张景芝,施智平,王国辉,关永.单球驱动平衡机器人运动学和动力学形式化验证.软件学报,2025,36(8):1-15

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:August 24,2024
  • Revised:October 14,2024
  • Online: December 10,2024
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063