Formal Foundations of 3D Geometry to Model Robot Manipulators

Abstract : We are interested in the formal specification of safety properties of robot manipulators down to the mathematical physics. To this end, we have been developing a formalization of the mathematics of rigid body transformations in the COQ proof-assistant. It can be used to address the forward kinematics problem, i.e., the computation of the position and orientation of the end-effector of a robot manipulator in terms of the link and joint parameters. Our formalization starts by extending the Mathematical Components library with a new theory for angles and by developing three-dimensional geometry. We use these theories to formalize the foundations of robotics. First, we formalize a comprehensive theory of three-dimensional rotations, including exponentials of skew-symmetric matrices and quaternions. Then, we provide a formalization of the various representations of rigid body transformations: isometries, homogeneous representation, the Denavit-Hartenberg convention, and screw motions. These ingredients make it possible to formalize robot manipulators: we illustrate this aspect by an application to the SCARA robot manipulator.
Type de document :
Communication dans un congrès
Conference on Certified Programs and Proofs 2017, Jan 2017, Paris, France
Liste complète des métadonnées

Littérature citée [24 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01414753
Contributeur : Cyril Cohen <>
Soumis le : lundi 12 décembre 2016 - 15:18:50
Dernière modification le : jeudi 11 janvier 2018 - 17:01:48
Document(s) archivé(s) le : mardi 28 mars 2017 - 00:01:27

Fichier

robot_cpp_final.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01414753, version 1

Collections

Citation

Reynald Affeldt, Cyril Cohen. Formal Foundations of 3D Geometry to Model Robot Manipulators. Conference on Certified Programs and Proofs 2017, Jan 2017, Paris, France. 〈hal-01414753〉

Partager

Métriques

Consultations de la notice

416

Téléchargements de fichiers

423