skip to main content
10.1145/3018610.3018629acmotherconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
research-article

Formal foundations of 3D geometry to model robot manipulators

Published: 16 January 2017 Publication History

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.

References

[1]
R. Affeldt and C. Cohen. Formal foundations of 3D geometry to model robot manipulators. https://staff.aist.go.jp/ reynald.affeldt/documents/robot_cpp_long.pdf, Nov. 2016. Long version of this paper. A. Anand and R. A. Knepper. ROSCoq: Robots powered by constructive reals. In 6th International Conference on Interactive Theorem Proving (ITP 2015), Nanjing, China, August 24–27, 2015, volume 9236 of LNCS, pages 34–50. Springer, 2015.
[2]
C. Auger, Z. Bouzid, P. Courtieu, S. Tixeuil, and X. Urbain. Certified impossibility results for byzantine-tolerant mobile robots. In 15th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS 2013), Osaka, Japan, November 13– 16, 2013, volume 8255 of LNCS, pages 178–190. Springer, Nov. 2013.
[3]
C. Cohen. Construction of real algebraic numbers in Coq. In 3rd International Conference on Interactive Theorem Proving (ITP 2012), Princeton, NJ, USA, August 13–15, 2012, volume 7406 of LNCS, pages 67–82. Springer, 2012a. C. Cohen. Formalized algebraic numbers: construction and firstorder theory. PhD thesis, Ecole Polytechnique X, Nov. 2012b. C. Cohen, M. Dénès, and A. Mörtberg. Refinements for free! In 3rd International Conference on Certified Programs and Proofs (CPP 2013), Melbourne, VIC, Australia, December 11–13, 2013, volume 8307 of LNCS, pages 147–162. Springer, 2013.
[4]
P. Courtieu, L. Rieg, S. Tixeuil, and X. Urbain. Impossibility of gathering, a certification. Information Processing Letters, 115(3): 447–452, 2015.
[5]
P. Courtieu, L. Rieg, S. Tixeuil, and X. Urbain. Certified universal gathering in R 2 for oblivious mobile robots. In 30th International Symposium on Distributed Computing (DISC 2016), Paris, France, September 27–29, 2016, volume 9888 of LNCS, pages 187–200. Springer, Sep. 2016.
[6]
L. Cruz-Filipe, H. Geuvers, and F. Wiedijk. C-CoRN: the constructive Coq repository at Nijmegen. In 3rd International Conference on Mathematical Knowledge Management (MKM 2004), Bialowieza, Poland, September 19–21, 2004, volume 3119 of LNCS, pages 88–103. Springer, 2004.
[7]
M. Dénès. Étude formelle d’algorithmes efficaces en algèbre linéaire. PhD thesis, Université de Nice - Sophia Antipolis, Nov. 2013.
[8]
M. Dénès, A. Mörtberg, and V. Siles. A refinement-based approach to computational algebra in Coq. In 3rd International Conference on Interactive Theorem Proving (ITP 2012), Princeton, NJ, USA, August 13–15, 2012, volume 7406 of LNCS, pages 83–98. Springer, 2012.
[9]
B. Farooq, O. Hasan, and S. Iqbal. Formal kinematic analysis of the two-link planar manipulator. In 15th International Conference on Formal Engineering Methods (ICFEM 2013), Queenstown, New Zealand, October 29–November 1, 2013, volume 8144 of LNCS, pages 347–362, 2013.
[10]
F. Garillot, G. Gonthier, A. Mahboubi, and L. Rideau. Packaging Mathematical Structures. In 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2009), Munich, Germany, August 17–20, 2009, volume 5674 of LNCS. Springer, 2009.
[11]
G. Gonthier, A. Asperti, J. Avigad, Y. Bertot, C. Cohen, F. Garillot, S. L. Roux, A. Mahboubi, R. O’Connor, S. O. Biha, I. Pasca, L. Rideau, A. Solovyev, E. Tassi, and L. Théry. A machinechecked proof of the odd order theorem. In 4th International Conference on Interactive Theorem Proving (ITP 2013), Rennes, France, July 22–26, 2013, volume 7998 of LNCS, pages 163–179, 2013.
[12]
J. Harrison. The HOL Light theory of euclidean space. Journal of Automated Reasoning, 50:173–190, 2013.
[13]
H. Herencia-Zapana, R. Jobredeaux, S. Owre, P. Garoche, E. Feron, G. Perez, and P. Ascariz. PVS linear algebra libraries for verification of control software algorithms in C/ACSL. In 4th International Symposium NASA Formal Methods (NFM 2012), Norfolk, VA, USA, April 3–5, 2012, volume 7226 of LNCS, pages 147–161. Springer, Apr. 2012.
[14]
C. Kaliszyk and R. O’Connor. Computing with classical real numbers. CoRR, abs/0809.1644, 2008.
[15]
S. Ma, Z. Shi, Z. Shao, Y. Guan, L. Li, and Y. Li. Higher-order logic formalization of conformal geometric algebra and its application in verifying a robotic manipulation algorithm. Advances in Applied Clifford Algebras, 26(4):1305–1330, Dec. 2016.
[16]
R. M. Murray, Z. Li, and S. S. Sastry. A Mathematical Introduction to Robotic Manipulation. CRC Press, 1994. 1st edition. B. O’Neill. Elementary Differential Geometry. Academic Press, 1966.
[17]
F. C. Park and K. Lynch. Introduction to robotics: Mechanics, planning, and control. Technical report, Seoul National University, 2012. Course text. B. Siciliano and O. Khatib, editors. Springer Handbook of Robotics. Springer, 2008.
[18]
B. Spitters and E. van der Weegen. Type classes for mathematics in type theory. Mathematical Structures in Computer Science, 21 (4):795–825, 2011.
[19]
M. W. Spong, S. Hutchinson, and M. Vidyasagar. Robot Modeling and Control. John Wiley & Sons, 2006.
[20]
The Coq Development Team. Reference manual. Available at http://coq.inria.fr, 1999–2016. INRIA. Ver. 8.5pl2. D. Walter, H. Täubig, and C. Lüth. Experiences in applying formal verification in robotics. In 29th International Conference on Computer Safety, Reliability, and Security (SAFECOMP 2010), Vienna, Austria, September 14–17, 2010, volume 6351 of LNCS, pages 347–360, 2010.

Cited By

View all
  • (2024)Formal Kinematic Analysis of Epicyclic Bevel Gear TrainsFormal Methods and Software Engineering10.1007/978-981-96-0617-7_10(162-180)Online publication date: 29-Nov-2024
  • (2024)Coq Formalization of Orientation Representation: Matrix, Euler Angles, Axis-Angle and QuaternionFormal Aspects of Component Software10.1007/978-3-031-71261-6_5(79-96)Online publication date: 9-Sep-2024
  • (2024)Formally verified asymptotic consensus in robust networksTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-031-57246-3_14(248-267)Online publication date: 4-Apr-2024
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Other conferences
CPP 2017: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs
January 2017
234 pages
ISBN:9781450347051
DOI:10.1145/3018610
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

In-Cooperation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 16 January 2017

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. 3D Geometry
  2. Coq
  3. Formal verification
  4. Proof-assistant
  5. Robot manipulator

Qualifiers

  • Research-article

Conference

CPP '17
CPP '17: Certified Proofs and Programs
January 16 - 17, 2017
Paris, France

Acceptance Rates

Overall Acceptance Rate 18 of 26 submissions, 69%

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)17
  • Downloads (Last 6 weeks)0
Reflects downloads up to 19 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2024)Formal Kinematic Analysis of Epicyclic Bevel Gear TrainsFormal Methods and Software Engineering10.1007/978-981-96-0617-7_10(162-180)Online publication date: 29-Nov-2024
  • (2024)Coq Formalization of Orientation Representation: Matrix, Euler Angles, Axis-Angle and QuaternionFormal Aspects of Component Software10.1007/978-3-031-71261-6_5(79-96)Online publication date: 9-Sep-2024
  • (2024)Formally verified asymptotic consensus in robust networksTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-031-57246-3_14(248-267)Online publication date: 4-Apr-2024
  • (2021)Mechanization of Incidence Projective Geometry in Higher Dimensions, a Combinatorial ApproachElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.352.8352(77-90)Online publication date: 30-Dec-2021
  • (2020)Toward the Formalization of Macroscopic Models of Traffic Flow Using Higher-Order-Logic Theorem ProvingIEEE Access10.1109/ACCESS.2020.29716618(27291-27307)Online publication date: 2020
  • (2020)Formalization of Camera Pose Estimation Algorithm based on Rodrigues FormulaFormal Aspects of Computing10.1007/s00165-020-00520-532:4-6(417-437)Online publication date: 1-Nov-2020
  • (2020)Formal Verification of Cyber-Physical Systems Using Theorem ProvingFormal Techniques for Safety-Critical Systems10.1007/978-3-030-46902-3_1(3-18)Online publication date: 26-Apr-2020
  • (2018)Formal analysis of the kinematic Jacobian in screw theoryFormal Aspects of Computing10.1007/s00165-018-0468-030:6(739-757)Online publication date: 1-Nov-2018
  • (2017)Formal foundations of 3D geometry to model robot manipulatorsProceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs10.1145/3018610.3018629(30-42)Online publication date: 16-Jan-2017

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media