Formal verification secures tilt estimation in humanoid robots
Formal verification of tilt estimation using the Rocq prover
Logic in Computer Science
Summary
Knowing which way is up is very important for robots that walk on two legs. This paper builds trusted math tools in a proof system called Rocq to guarantee that methods estimating a robot's tilt are correct and stable. The authors create a formal framework to analyze differential equations and prove that these estimations behave reliably over time. Finally, they use these tools to verify a state-of-the-art tilt estimator for humanoid robots.
What this means in practice
- •For robotics engineers: Ensure the reliability and correctness of tilt estimation algorithms used in humanoid robots by applying formally verified stability proofs.
- •For control systems designers: Use the formal stability analysis libraries developed here to build and verify more robust control systems involving dynamical models.
Authors
Reynald Affeldt, Lynda Bentoucha, Yoshihiro Ishiguro, Holger Thies
Abstract
The safe operation of a humanoid robot critically relies on accurate estimation of its vertical orientation, or ``tilt''. This requires a variety of mathematical tools, including three-dimensional geometry and differential equations. To formally verify tilt estimation, we develop a library for stability analysis in the Rocq prover. We start by formalizing a theory of ordinary differential equations. We provide a formalization of the (local) Cauchy-Lipschitz (a.k.a. Picard-Lindelof) theorem for existence and uniqueness, taking advantage of the library support for quotients provided by the Mathematical Components library. We extend this formalization with a variant for global existence and continuous dependence on initial conditions. Building on these foundations, we develop a theory of Lyapunov stability that is compatible with an existing formalization of LaSalle's invariance principle. We also extend an existing library for the statics of robot manipulators to support dynamical systems. Finally, we apply these libraries to the verification of a state-of-the-art tilt estimation developed for a humanoid robot.