Formal Verification of Robotic Cell Injection systems up to 4-DOF using HOL Light


Cell injection is an approach used for the delivery of small sample substances into a biological cell and is widely used in drug development, gene injection, intracytoplasmic sperm injection and in-vitro fertilization. Robotic cell injection systems provide the automation of the process as opposed to the manual and semi-automated cell injection systems, which require expert operators and involve time consuming processes and also have lower success rates. The automation of the cell injection process is obtained by controlling the orientation and movement of its various components, like injection manipulator, microscope etc., and planning the motion of the injection pipette by controlling the force of the injection. The conventional techniques to analyze the cell injection process include paper-and-pencil proof and computer simulation methods. However, both these techniques suffer from their inherent limitations, such as, proneness to human error for the former and the approximation of the mathematical expressions involved in the numerical algorithms for the latter. Formal methods have the capability to overcome these limitations and can provide an accurate analysis of these cell injection systems. Model checking, i.e., a state-based formal method, has been recently used for analyzing these systems. However, it involves the discretization of the differential equations capturing the continuous dynamics of the system and thus compromises on the completeness of the analysis of these safety-critical systems. In this paper, we propose a higher-order-logic theorem proving (a deductive-reasoning based formal method) based framework for analyzing the dynamical behavior of the robotic cell injection systems upto 4-DOF. The proposed analysis, based on the HOL Light theorem prover, enabled us to identify some discrepancies in the simulation and model checking based analysis of the same robotic cell injection system.

This is a preview of subscription content, log in to check access.


  1. [AH17]

    Ayub MS, Hasan O (2017) Formal probabilistic analysis of a virtual fixture control algorithm for a surgical robot. In: Verification and evaluation of computer and communication systems, volume 10466 of LNCS, pp 1–16. Springer

  2. [BDA95]

    Bianco A, De Alfaro L (1995) Model checking of probabilistic and nondeterministic systems. I:n Foundations of software technology and theoretical computer science, volume 1026 of LNCS, pp 499–513. Springer

  3. [BGM+15]

    Bresolin, D., Geretti, L., Muradore, R., Fiorini, P., Villa, T.: Formal verification of robotic surgery tasks by reachability analysis. Microprocess Microsyst 39(8), 836–842 (2015)

    Article  Google Scholar 

  4. [CGP99]

    Clarke, E.M., Grumberg, O., Peled, D.: Model checking. MIT Press (1999)

  5. [CKNZ12]

    Clarke EM, Klieber W, Nováček M, Zuliani P (2012) Model checking and the state explosion problem. In: Tools for practical software verification, volume 7682 of LNCS, pp 1–30. Springer

  6. [Daw11]

    Dawood H (2011) Theories of interval arithmetic: mathematical foundations and applications. LAP Lambert Academic Publishing

  7. [DPV13]

    Durán AJ, Pérez M, Varona JL (2013) The misfortunes of a mathematicians' Trio using computer algebra systems: can we trust? CoRR. arXiv:1312.3270

  8. [FN16]

    Faroque M, Nizam S (2016) Virtual reality training for micro-robotic cell injection. Technical report, Deakin University, Australia

  9. [Gor88]

    Gordon Michael JC (1988) HOL: a proof generating system for higher-order logic. In: VLSI specification, verification and synthesis, volume 35 of SECS, pp 73–128. Springer

  10. [Har96a]

    Harrison J (1996) HOL light: a tutorial introduction. In: Srivas M, Camilleri A (eds) Proceedings of the first international conference on formal methods in computer-aided design (FMCAD'96), volume 1166 of LNCS, pp 265–269. Springer-Verlag

  11. [Har96b]

    Harrison J (1996) HOL light: a tutorial introduction. In: Formal methods in computer-aided design, volume 1166 of LNCS, pp 265–269. Springer

  12. [Har09]

    Harrison, J.: Handbook of practical logic and automated reasoning. Cambridge University Press (2009)

  13. [Har13]

    Harrison J(2013) The HOL light theory of euclidean space. J Autom Reason 1–18

  14. [hol20a]

    HOL Light Multivariate Calculus (2020)

  15. [hol20b]

    HOL Light Real Calculus (2020)

  16. [hol20c]

    HOL Light Transcendentals (2020)

  17. [hol20d]

    HOL Light Vectors and Matrices (2020)

  18. [HSM+09]

    Huang, H., Sun, D., Mills, J.K., Li, W.J., Cheng, S.H.: Visual-based impedance control of out-of-plane cell injection systems. Trans Autom Sci Eng 6(3), 565–571 (2009)

    Article  Google Scholar 

  19. [HSML06]

    Huang H, Sun D, Mills JK, Li Wen J (2006) A visual impedance force control of a robotic cell injection system. In: Robotics and biomimetics, pp 233–238. IEEE

  20. [HT15]

    Hasan O, Tahar S (2015) Formal verification methods. In: Encyclopedia of information science and technology, pp 7162–7170. IGI Global Pub

  21. [KK04]

    Kuncova J, Kallio Pasi (2004) Challenges in capillary pressure microinjection. In: Engineering in Medicine and Biology Society, volume 2, pp 4998–5001. IEEE

  22. [KRPK13]

    Kouskoulas Y, Renshaw D, Platzer A, Kazanzides P (2013) Certifying the safe design of a virtual fixture control algorithm for a surgical robot. In: Hybrid systems: computation and control, pp 263–272. ACM

  23. [Map20]

    Maple (2020)

  24. [Mat20]

    Mathematica (2020)

  25. [NFT+98]

    Nakayama, T., Fujiwara, H., Tastumi, K., Fujita, K., Higuchi, T., Mori, T.: A new assisted hatching technique using a piezo-micromanipulator. Fertil Steril 69(4), 784–788 (1998)

    Article  Google Scholar 

  26. [NS94]

    Nethery, J.F., Spong, M.W.: Robotica: a mathematica package for robot analysis. IEEE Robot Autom Mag 1(1), 13–20 (1994)

    Article  Google Scholar 

  27. [Pau96]

    Paulson, L.C.: ML for the working programmer. Cambridge University Press (1996)

  28. [Ras20]

    Rashid A (2020) Formal verification of robotic cell injection systems upto \(4\)-DOF using HOL Light.

  29. [RH17]

    Rashid A, Hasan O (2017) Formal analysis of robotic cell injection systems using theorem proving. In: Design, modeling, and evaluation of cyber physical systems, volume 11267 of LNCS, pp 127–141. Springer

  30. [RH18]

    Rashid A, Hasan O (2018) Formal modeling of robotic cell injection systems in higher-order logic. In: Formal verification of physical systems, volume 2307, pp 1–9. CEUR-WS

  31. [SH17]

    Sardar MU, Hasan O (2017) Towards probabilistic formal modeling of robotic cell injection systems. In: Models for formal analysis of real systems, pp 271–282

  32. [SL97]

    Sun D, Liu Y (1997) Modeling and impedance control of a two-manipulator system handling a flexible beam. In: Proceedings of 1997 IEEE International Conference on Robotics and automation, volume 2, pp 1787–1792. IEEE

  33. [SN02]

    Sun, Y., Nelson, B.J.: Biological cell injection using an autonomous microrobotic system. Robot Res 21(10–11), 861–868 (2002)

    Article  Google Scholar 

  34. [YKY+99]

    Yanagida, K., Katayose, H., Yazawa, H., Kimura, Y., Konnai, K., Sato, A.: The usefulness of a piezo-micromanipulator in intracytoplasmic sperm injection in humans. Hum Reprod 14(2), 448–453 (1999)

    Article  Google Scholar 

Download references

Author information



Corresponding author

Correspondence to Adnan Rashid.

Additional information

Ana Cavalcanti and Pedro Ribeiro

Rights and permissions

Reprints and Permissions

About this article

Verify currency and authenticity via CrossMark

Cite this article

Rashid, A., Hasan, O. Formal Verification of Robotic Cell Injection systems up to 4-DOF using HOL Light. Form Asp Comp (2020).

Download citation


  • Robotic cell injection systems
  • Formal verification
  • Theorem proving
  • Higher-order logic
  • HOL Light