Abstract
Kinematic analysis is used for trajectory planning of robotic manipulators and is an integral step of their design. The main idea behind kinematic analysis is to study the motion of the robot based on the geometrical relationship of the robotic links and their joints. Given the continuous nature of kinematic analysis, traditional computer-based verification methods, such as simulation, numerical methods or model checking, fail to provide reliable results. This fact makes robotic designs error prone, which may lead to disastrous consequences given the safety-critical nature of robotic applications. Leveraging upon the high expressiveness of higher-order logic, we propose to use higher-order-logic theorem proving for conducting formal kinematic analysis. As a first step towards this direction, we utilize the geometry theory of HOL-Light to develop formal reasoning support for the kinematic analysis of a two-link planar manipulator, which forms the basis for many mechanical structures in robotics. To illustrate the usefulness of our foundational formalization, we present the formal kinematic analysis of a biped walking robot.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Avigad, J., Dean, E., Mumma, J.: A Formal System for Euclid’s Elements. Review of Symbolic Logic 2(4), 700–768 (2009)
Becker, B., Cardelli, L., Hermanns, H., Tahar, S.: Abstracts collection. In: Verification over Discrete-Continuous Boundaries. Dagstuhl Seminar Proceedings, vol. 10271. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany (2010)
Binyameen, M.: Formal Kinematic Analysis of the Two-Link Planar Manipulator using HOL-Light (2013), http://save.seecs.nust.edu.pk/students/binyameen/tlpm.html
Chivarov, N., Galabov, V.: Kinematics of Scara Robots. In: Problems of Engineering Cybernetics and Robotics, pp. 51–59 (2008)
Denavit, J., Hartenberg, R.S.: A Kinematic Notation for Lower-Pair Mechanisms based on Matrices. Trans. ASME Journal of Applied Mechanics 23, 215–221 (1955)
Esposito, J.M., Moonzoo, K.: Using Formal Modeling with an Automated Analysis Tool to Design and Parametrically Analyze a Multirobot Coordination Protocol: A Case Study. IEEE Transactions on Systems, Man and Cybernetics, Part A: Systems and Humans 37(3), 285–297 (2007)
Fryziel, L., Fried, G., Djouani, K., Iqbal, S., Amirat, Y.: A Kinematic Analysis for a Hybrid Continuum Active Catheter. In: Proceedings of the 7th France-Japon Congress 5th Europe-Asia Congress on Mechatronics (MECHATRONICS 2008), Le Grand Bornand, France (2008)
Haddadin, S., Albu-Schäffer, A., Hirzinger, G.: Requirements for Safe Robots: Measurements, Analysis and New Insights. International Journal of Robotics Research 28(11-12), 1507–1527 (2009)
Harrison, J.: The HOL Light Theory of Euclidean Space. Automated Reasoning 50(2), 173–190 (2013)
Hurmuzlu, Y., Ganot, F., Brogliato, B.: Modeling, Stability and Control of Biped Robots: general framework. Automatica 10 (2004)
Iqbal, S., Mohammed, S., Amirat, Y.: A Guaranteed Approach for Kinematic Analysis of Continuum Robot Based Catheter. In: Robotics and Biomimetics, pp. 1573–1578 (2009)
Lum, H.K., Zirbi, M., Soh, Y.C.: Planning and Control of a Biped Robot. International Journal of Engineering Science 37, 1319–1349 (1999)
Merlet, J.P.: A Formal Numerical Approach for Robust In-Workspace Singularity Detection. IEEE Transactions on Robotics 23, 393–402 (2007)
Myszka, D.: Machines and Mechanisms: Applied Kinematic Analysis, 4th edn. Prentice Hall (2011)
Petrovic, D., Maric, F.: Formalizing Analytic Geometries. In: Automated Deduction in Geometry (2012)
Pham, T.-M., Bertot, Y., Narboux, J.: A Coq-based Library for Interactive and Automated Theorem Proving in Plane Geometry. In: Murgante, B., Gervasi, O., Iglesias, A., Taniar, D., Apduhan, B.O. (eds.) ICCSA 2011, Part IV. LNCS, vol. 6785, pp. 368–383. Springer, Heidelberg (2011)
Proetzsch, M., Berns, K., Schuele, T., Schneider, K.: Formal Verification of Safety Behaviours of the Outdoor Robot RAVON. In: Informatics in Control, Automation and Robotics, pp. 157–164 (2007)
Ras, J., Cheng, A.M.K.: On Formal Verification of Toyota’s Electronic Throttle Controller. In: Systems Conference, SysCon (2011)
Shores, B.E., Minor, M.A.: Design, Kinematic Analysis, and Quasi-steady Control of a Morphic Rolling Disk Biped Climbing Robot. In: Robotics and Automation, pp. 2721–2726 (2005)
Sloth, C.: Formal Verification of Continuous Systems. PhD thesis, Aalborg University (2013)
Sloth, C., Wisniewski, R.: Abstractions for Mechanical Systems. IFAC Workshop Series, pp. 96–101 (2012)
Spong, M.W., Hutchinson, S., Vidyasagar, M.: Robot Modeling and Control, 1st edn. Wiley (2005)
Walter, D., Täubig, H., Lüth, C.: Experiences in applying Formal Verification in Robotics. In: Schoitsch, E. (ed.) SAFECOMP 2010. LNCS, vol. 6351, pp. 347–360. Springer, Heidelberg (2010)
Wang, Y., Chirikjian, G.S.: Propagation of Errors in Hybrid Manipulators. In: International Conference on Robotics and Automation, pp. 1848–1853 (2006)
Wolfram Research. Mathematica Mechanical Systems: Kinematic and Dynamic Analysis in Mathematica, 3rd edn. (2005), http://www.wolfram.com
Yoshikawa, T.: Manipulability of Robotic Mechanisms. The International Journal of Robotics Research 4(2), 3–9 (1985)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Farooq, B., Hasan, O., Iqbal, S. (2013). Formal Kinematic Analysis of the Two-Link Planar Manipulator. In: Groves, L., Sun, J. (eds) Formal Methods and Software Engineering. ICFEM 2013. Lecture Notes in Computer Science, vol 8144. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-41202-8_23
Download citation
DOI: https://doi.org/10.1007/978-3-642-41202-8_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-41201-1
Online ISBN: 978-3-642-41202-8
eBook Packages: Computer ScienceComputer Science (R0)