Formal verification of robotic cell injection systems up to 4-DOF using HOL Light.

*(English)*Zbl 1458.68220Summary: 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.

##### MSC:

68T40 | Artificial intelligence for robotics |

68Q60 | Specification and verification (program logics, model checking, etc.) |

68V15 | Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) |

##### Keywords:

robotic cell injection systems; formal verification; theorem proving; higher-order logic; HOL Light
PDF
BibTeX
XML
Cite

\textit{A. Rashid} and \textit{O. Hasan}, Formal Asp. Comput. 32, No. 2--3, 229--250 (2020; Zbl 1458.68220)

Full Text:
DOI

##### References:

[1] | 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] | 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 · Zbl 1354.68167 |

[3] | 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) |

[4] | Clarke, E.M., Grumberg, O., Peled, D.: Model checking. MIT Press (1999) · Zbl 1423.68002 |

[5] | 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] | Dawood H (2011) Theories of interval arithmetic: mathematical foundations and applications. LAP Lambert Academic Publishing |

[7] | 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 · Zbl 1338.68299 |

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

[9] | 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] | 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] | Harrison J (1996) HOL light: a tutorial introduction. In: Formal methods in computer-aided design, volume 1166 of LNCS, pp 265-269. Springer |

[12] | Harrison, J.: Handbook of practical logic and automated reasoning. Cambridge University Press (2009) · Zbl 1178.03001 |

[13] | Harrison J(2013) The HOL light theory of euclidean space. J Autom Reason 1-18 · Zbl 1260.68373 |

[14] | HOL Light Multivariate Calculus (2020) https://github.com/jrh13/hol-light/blob/master/Multivariate |

[15] | HOL Light Real Calculus (2020) https://github.com/jrh13/hol-light/blob/master/Multivariate/realanalysis.ml |

[16] | HOL Light Transcendentals (2020) https://github.com/jrh13/hol-light/blob/master/Multivariate/transcendentals.ml |

[17] | HOL Light Vectors and Matrices (2020) https://github.com/jrh13/hol-light/blob/master/Multivariate/vectors.ml |

[18] | Huang, H.; Sun, D.; Mills, JK; Li, WJ; Cheng, SH, Visual-based impedance control of out-of-plane cell injection systems, Trans Autom Sci Eng, 6, 3, 565-571 (2009) |

[19] | 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] | Hasan O, Tahar S (2015) Formal verification methods. In: Encyclopedia of information science and technology, pp 7162-7170. IGI Global Pub |

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

[22] | 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] | Maple (2020) https://www.maplesoft.com/ |

[24] | Mathematica (2020) https://www.wolfram.com/mathematica/ |

[25] | 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) |

[26] | Nethery, JF; Spong, MW, Robotica: a mathematica package for robot analysis, IEEE Robot Autom Mag, 1, 1, 13-20 (1994) |

[27] | Paulson, L.C.: ML for the working programmer. Cambridge University Press (1996) · Zbl 0863.68032 |

[28] | Rashid A (2020) Formal verification of robotic cell injection systems upto \(4\)-DOF using HOL Light. http://save.seecs.nust.edu.pk/fvrcis/ |

[29] | 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] | 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] | 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] | 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] | Sun, Y.; Nelson, BJ, Biological cell injection using an autonomous microrobotic system, Robot Res, 21, 10-11, 861-868 (2002) |

[34] | 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) |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.