Robotic cell injection is used for automatically delivering substances into a cell and is an integral component of drug development, genetic engineering and many other areas of cell biology. Traditionally, the correctness of functionality of these systems is ascertained using paperand-pencil proof and computer simulation methods. However, the paper based proofs can be human-error prone and the simulation provides an incomplete analysis due to its sampling based nature and the inability to capture continuous behaviors in computer based models. Model checking has been recently advocated for the analysis of cell injection systems as well. However, it involves the discretization of the di erential equations that are used for modeling the dynamics of the system and thus compromises on the completeness of the analysis as well. In this paper, we propose to use higher-order-logic theorem proving for the modeling and analysis of the dynamical behaviour of the robotic cell injection systems. The high expressiveness of the underlying logic allows us to capture the continuous details of the model in their true form. Then, the model can be analyzed using deductive reasoning within the sound core of a proof assistant.
Robotic cell injection systems are used to automatically and precisely insert small amounts of substances, such as molecules and genes, into cells during various gene injection [KK04], drug development [NFT+98], intracytoplasmic sperm injection (ISCI) [YKY+99] and in-vitro fertilization (IVF) [SN02]. The most critical factor in these systems is the precision and accuracy of the injection force [HSM+09] as a slight excessive force may damage the membrane of the cell [HSML06] or an insu cient force may not be able to pierce the cell [FN16]. Moreover, these robotic systems consist of many sub-components, like injection manipulator, digital cameras, sensors and microscope optics [HSM+09], and a controlled movement of these fundamental components is also quite vital for the functionality of the overall system.
In order to attain the above-mentioned objectives, the robotic cell injection systems need to be carefully designed and analyzed. For this purpose, the behavior of a robotic cell injection system's movements has to be modeled using the coordinate frames corresponding to the orientations of its various components, i.e., the injection manipulator, cameras and images. Similarly, we need to capture the motion planning of the injection pipette in terms of force control algorithms, such as the contact-space-impedance force control [SL97, HSM+09] and the image-based torque controller [HSML06]. These models are then analyzed to ensure the desired behavior using paper-and-pencil and simulation techniques. However, the manual analytical analysis is prone to human error and also is not scalable for analyzing complex robotic cell injection systems. Similarly, due to the continuous nature of the analysis and the limited amount of computational resources, the system is analyzed for a certain number of test cases only in simulation and thus the absolute accuracy cannot be achieved. Thus, the abovementioned traditional techniques cannot be relied upon as they are either error prone or incomplete, which may lead to an undetected error in the analysis that may in turn lead to disastrous consequences given the safety-critical nature of robotic cell injection systems.
Formal methods [HT15] are computer-based mathematical analysis techniques that can overcome the abovementioned inaccuracies. Primarily, these techniques involve the development of a mathematical model of a system and veri cation of its properties using computer-based mathematical reasoning. Sardar et al. [SH17] recently used probabilistic modeling checking [CGP99], i.e., a state-based formal method, to formally analyze the robotic cell injection systems. However, their methodology involves the discretization of the di erential equations that model the dynamics of these systems, which compromises the accuracy of the corresponding analysis. Moreover, the analysis also su ers from the inherent state-space explosion problem [CKNZ12]. Higher-order-logic theorem proving [Har09] is an interactive veri cation technique that can overcome these limitations. It primarily involves the mathematical modeling of the system based on higher-order logic and veri cation of its properties based on deductive reasoning. Given the high expressiveness of higher-order logic, it can truly capture the behavior of the di erential equations, which is not possible in model checking based analysis.
In this paper, we propose to use the higher-order-logic theorem proving to formally model and analyze the robotic cell injection systems [HSML06] using the HOL Light proof assistant [Har96]. The main motivation for the selection of HOL Light is the availability of reasoning support for real calculus [hol18b], multivariate calculus [hol18a], vectors [hol18a] and matrices [hol18a], which are some of the foremost requirements for formally analyzing robotic cell injection systems. We use these foundations to formally model the camera, stage and image coordinates and formal veri cation of their interrelationships in HOL Light. Similarly, we also formally modeled the dynamics of two degrees of freedom (DOF) motion stage using a system of di erential equations and the formal veri cation of their solutions.
The rest of the paper is organized as follows: Section 2 provides an introduction about the multivariate calculus theories of HOL Light that we build upon to model the robotic cell injection system. We provide an overview about the robotic cell injection system in Section 3. Section 4 presents the formalization of robotic cell injection system. Finally, Section 5 concludes the paper. 2
A N-dimensional vector in HOL Light is modeled as a RN column matrix with each of its element representing a real number [Har13]. All of the vector arithmetics are thus done using matrix manipulations. Similarly, all theorems of HOL Light multivariable calculus theories are veri ed for functions with an arbitrary data-type RN ! RM.
We explain some of the frequently used HOL Light functions in the proposed formalization as follows: De nition 2.1. Vector ` 8 l. vector l = (lambda i. EL (i - 1) l) The function vector takes an arbitrary list l : list and results into a vector having each component of data-type . It uses the HOL Light function EL n L, which extracts the nth element of a list L. Here, the lambda operator in HOL is used for constructing a vector based on its components [Har13].
` 8 x. cos x = Re (ccos (Cx x)) ` 8 x. sin x = Re (csin (Cx x))
The functions cos : R ! R and sin : R ! R in HOL Light represent the real cosine and real sine [hol18c], respectively. These functions are modeled in HOL Light based on the complex cosine ccos : R2 ! R2 and complex sine csin : R2 ! R2 functions, respectively.
` 8 f x. real derivative f x = (@f0. (f has real derivative f0) (atreal x))
The function real derivative represents the derivative of a real-valued function and is de ned using the Hilbert choice operator @ in the functional form. It accepts a real-valued function f : R ! R and a real number x, which is the point at which f has to be di erentiated, and returns a variable of data-type R, which is the di erential of f at x. The function has real derivative de nes the same relationship in the relational form.
We build upon the above-mentioned fundamental functions of multivariable calculus to formally analyze the robotic cell injection system in Section 4 of the paper. 3
A typical robotic cell injection system is composed of three modules, namely executive, sensory and control modules as depicted in Figure 1. The executive module comprises of working plate, positioning table and the injection manipulator. The working plate is mounted on the positioning table (XY -axis) and thus holds the cells that need to be injected. Similarly, the injection manipulator is mounted on Z-axis as shown in Figure 1.
The sensory module consists of a vision system that has four components, namely charged coupled device (CCD) camera, processing card, peripheral component interconnect (PCI) image capture and an optical microscope. A PCI image capture alongside a CCD camera is used to capture the process of cell injection. The control module includes a DCT0040 motion control system and a host computer. The con guration of a robotic cell injection system is depicted in Figure 2. The stage (table and working plate) coordinate frame is represented as the axis o xyz, where the origin of these coordinates, i.e., o represents the center of the working plate and the optical axis of the microscope is along the component z of the axis. Similarly, the camera coordinate frame is represented by the axis oc xcyczc, where the origin oc represents the center of the microscope. The axis oi uv
e l u d o M y r Microscope o s n e S Working plate e l u d o M e v i t u c e xE X-Y Table X
Z
Y
θ Z s i x a Z
e l u d o M l o r t n o C represents the coordinate frame in image plane with oi representing its origin and the axis uv is perpendicular to the optical axis.
v oi θi u yc zc oc
xc o y z x
θ This section presents the higher-order-logic based formal modeling of the robotic cell injection system. To facilitate the understanding of the paper for a non-HOL user, we use the standard mathematical notations for describing the proposed formalization rather than the HOL Light notations. However, the readers, interested in viewing the exact HOL Light formalization, can nd the source code of our formalization at [Ras18]. We consider 2-DOF to capture the dynamics of the robotic cell injection system. The stage, camera and image coordinates are two-dimensional coordinates, which are formalized in HOL Light as:
` 8 x y t. two dim coordinates x y t = x(t) y(t) where x : R ! R and y : R ! R modeling the respective axes and t is a variable representing the time.
Next, we formalize the two-dimensional displacement vector between the origins of the stage coordinate frame (o xyz) and the camera coordinate frame (oc xxyczc), and the rotation matrix from the stage coordinate frame to the camera coordinate frame as:
De nition 4.2. Displacement Vector and Rotation Matrix
dx ` 8 dx dy. displace vector dx dy = dy ` 8 alpha. rotat matrix alpha = cos (alpha) -sin (alpha)
The veri cation of the relationship between the camera, image and stage coordinate frames provides the reliable working of the robotic cell injection system as it ascertains the accuracy of the orientation and movement of its various modules, i.e., camera, microscope, stage frame and the injection manipulator. Firstly, we verify the relationship between camera and stage coordinates:
Theorem 4.1. Relationship Between Camera and Stage Coordinate Frames ` 8 xc yc x y alpha dx dy t.
[A1]: 0 < dx ^ [A2]: 0 < dy ) relat camera stage coordinates xc yc x y alpha dx dy t , xycc((tt)) = -x(xt()t) cos (alpha) + y(t) sin (alpha) + y(t) sin (alpha) + dx ! cos (alpha) + dy where the function relat camera stage coordinates presents the camera-stage coordinate frame interrelationship. The assumptions A1 and A2 of the above theorem model the design constraints for the relationship. The proof process of Theorem 4.1 is based on the properties of vectors and matrices alongside some real arithmetic reasoning. Next, to verify the image-camera coordinate frame interrelationship, we rst formalize the display resolution matrix in HOL Light as:
` 8 fx fy. dis resol matrix fx fy = fx 0 0 fy Now, we verify the relationship between image and camera coordinate frames as: Theorem 4.2. Relationship Between Image and Camera Coordinate Frames ` 8 xc yc u v t fx fy.
[A1]: 0 < fx ^ [A2]: 0 < fy ) relat image camera coordinates xc yc u v t fx fy , uv((tt)) = ffxy xc(t) ! yc(t) where the function relat image camera coordinates models the image-camera coordinate frame interrelationship. The assumptions A1 and A2 of the above theorem present the design constraints for the relationship. Next, we formalize the transformation matrix between image and stage coordinate frames, which is used in the veri cation of their interrelationship:
De nition 4.4. Transformation Matrix fx ` 8 fx fy alpha. transfor matrix fx fy alpha = -fy cos (alpha) sin (alpha) fx fy Now, we verify an important relationship between the image and stage coordinate frames as: Theorem 4.3. Relationship Between Image and Stage Coordinate Frames ` 8 x y u v t fx fy dx dy alpha xc yc.
[A1]: 0 < dx ^ [A2]: 0 < dy ^ [A3]: 0 < fx ^ [A4]: 0 < fy ^ [A5]: two dim coordinates u v t =
dis resol matrix fx fy [A6]: two dim coordinates xc yc t = rotat matrix alpha
two dim coordinates xc yc t ^ ) two dim coordinates u v t =
two dim coordinates x y t + displace vector dx dy transfor matrix fx fy alpha two dim coordinates x y t + ffxy dx dy where models the matrix-vector multiplication operator in HOL Light. The assumptions A1-A4 provide the design constraints for the image-stage coordinate interrelationship. The assumption A5 provides the imagecamera coordinate interrelationship. The assumption A6 presents the camera-stage coordinate interrelationship. The proof process of Theorem 4.3 is mainly based on Theorems 4.1 and 4.2 alongside some arithmetic reasoning on the vectors and matrices. The veri cation of these interrelationships ensures the correct orientation of the various important components of a robotic cell injection system, i.e., camera, working plate, microscope and the injection manipulator.
Next, we model and verify the dynamics of the robotic cell injection system. The dynamics of the 2-DOF motion stage is based on Lagrange's equation [Tho08] and mathematically represented as: mx + my + mp 0 my + mp 466 dd2ty 577 + 0 0 1 where mx, my and mp represent the masses of the xy positioning tables and working plate, respectively. Similarly, f exd and f eyd are the x and y components of the desired force applied to the actuators during the robotic cell injection process, respectively. Similarly, x and y are the x and y components of the input torque of the driving motor applied during the cell injection process, respectively. We formally model Equation (1) in HOL Light as: mx + my + mp 0
2 d2x 3 my + mp 466 dd2ty 577 + 0 0 1 dt
2 dx 3 0 6 dt 77 = 0 1 64 dy 5 0 dt We verify the solution of the above equation in HOL Light as the following theorem: (1) (2) De nition 4.5. Dynamics of the 2-DOF Motion Stage ` 8 mx my mp x y t taux tauy fexd feyd.
dynam 2 dof motion stage mx my mp x y t taux tauy fexd feyd , mass matrix mx my mp sec order deriv stage coordinates x y t + posit table matrix fir order deriv stage coordinates x y t =
torq vector taux tauy - desir force vector fexd feyd where mass matrix is the matrix containing the respective masses, i.e., mx, my and mp, and posit table matrix is a diagonal matrix. Similarly, desir force vector and torq vector are the desired force and the applied torque vectors, respectively, i.e., the elements of these vectors represent the components of the desired force and applied torque. The functions fir order deriv stage coordinates and sec order deriv stage coordinates represent the vectors containing rst-order and second-order derivatives of the stage coordinates, respectively: De nition 4.6. Vectors Containing First and Second-order Derivatives of the Stage Coordinates ` 8 x y t. fir order deriv stage coordinates x y t = deriv vector first [x; y] t ` 8 x y t. sec order deriv stage coordinates x y t = deriv vector second [x; y] t where deriv vector first and deriv vector second take a list containing the functions of data-type R ! R and output the vectors containing the corresponding rst and second-order derivatives of the functions. [Ras18].
If the desired force and the applied torque vectors are zero, then the injection pipette does not touch the cells. Thus, for this particular case, Equation (1) can be expressed as:
Theorem 4.4. Veri cation of Solution of Dynamical Behaviour of Motion Stage ` 8 x y mx my mp taux tauy fexd feyd alpha x0 y0 xd0 yd0.
[A1]: 0 < mx ^ [A2]: 0 < my ^ [A3]: 0 < mp ^
dx dy [A4]: x(0) = x0 ^ [A5]: y(0) = y0 ^ [A6]: (0)= xd0 ^ [A7]: dt dt [A8]: ffeeyxdd = 00 ^ [A9]: [A10]: (8 t. x(t) = (x0 + xd0 The assumptions A1-A3 provide the conditions on the masses mx, my and mp, i.e., all masses are positive. The assumptions A4-A7 present the values of coordinates x and y and their rst-order derivatives ddxt and ddyt at t = 0. The assumptions A8-A9 model the constraints on the components of the desired force and the torque, respectively, i.e., the desired force and torque vectors are zero. The assumptions A10-A11 present the values of xy coordinates at any time t. Finally, the conclusion provides the dynamical behaviour of the 2-DOF motion stage. The veri cation of Theorem 4.4 is mainly based on the properties of real derivatives, transcendental functions, vectors and matrices. Next, we verify an alternate representation of the image-stage coordinate interrelationship, which depends on the dynamical behaviour of the motion stage (De nition 4.5) and is an important property for analyzing cell injection systems. For this purpose, we rst formalize the inertia and positioning table matrices: De nition 4.7. Inertia and Positioning Table Matrices ` 8 mx my mp fx fy alpha. inertia matrix mx my mp fx fy alpha =
mass matrix mx my mp matrix inv (transfor matrix fx fy alpha) ` 8 fx fy alpha. posit table matrix fin fx fy alpha =
posit table matrix matrix inv (transfor matrix fx fy alpha) where the HOL Light function matrix inv takes a matrix A:RM N and returns its inverse (A 1). Now, we verify the alternate form of the relationship between image and stage coordinates in HOL Light: Theorem 4.5. Alternate Representation of the Image-Stage Coordinate Interrelationship ` 8 xc yc u v x y fx fy dx dy mx my mp taux tauy fexd feyd alpha. [A1]: 0 < dx ^ [A2]: 0 < dy ^ [A3]: 0 < fx ^ [A4]: 0 < fy ^ [A5]: invertible (transfor matrix fx fy alpha) ^ [A6]: (8 t. u real differentiable atreal t) ^ [A7]: (8 t. v real differentiable atreal t) ^
du [A8]: (8 t. real differentiable atreal t) ^ dt dv [A9]: (8 t. real differentiable atreal t) ^
dt [A10]: (8 t. relat image camera coordinates xc yc u v t fx fy) ^ [A11]: (8 t. relat camera stage coordinates xc yc x y alpha dx dy t) ^ [A12]: dynam 2 dof motion stage mx my mp x y t taux tauy fexd feyd ) inertia matrix mx my mp fx fy alpha sec order deriv image coordinates u v t + posit table matrix fin fx fy alpha fir order deriv image coordinates u v t = torq vector taux tauy - desir force vector fexd feyd
The assumptions A1-A4 present the design constraints for the relationship between the image and stage coordinates. The assumption A5 describes the invertibility of the transformation matrix transf mat, i.e., existence of its inverse. The assumptions A6-A9 provide the di erentiability conditions for the image coordinate and their rst-order derivatives. The assumptions A10-A11 represent the image-camera and camera-stage coordinates interrelationships. The assumption A12 provides the dynamical behavior of the 2-DOF motion stage. Finally, the conclusion of Theorem 4.5 presents the alternate form of the relationship between the image and stage coordinate frames. The proof process of the theorem is based on the properties of the real derivative, vectors and matrices alongwith some real arithmetic reasoning.
Due to the undecidable nature of the higher-order logic, the formalization presented in Section 4, involved manual interventions and human guidance. The proof e ort involved 520 lines-of-code and 12 man-hours. The details about the reported formalization can be found in our proof script [Ras18]. The distinguishing feature of our formalization is that all the veri ed theorems are universally quanti ed and can thus be specialized to the required values based on the requirement of the analysis of the cell injection systems. Moreover, our higher-order logic based approach allows us to model the dynamical behaviour of the robotic cell injection systems involving derivatives (Equation (1)) in their true form, whereas, they are discretized and modeled using a state-transition system in their model checking based analysis [SH17], which may compromise the correctness and completeness of the corresponding analysis. 5
In this paper, we proposed formal modeling of robotic cell injection systems in higher-order logic. We rst formalized the camera, image and stage coordinate frames, which are the vital components of a robotic cell injection system, and formally veri ed their interrelationship using the HOL Light proof assistant. We also formalized the dynamical behaviour of the 2-DOF motion stage based on di erential equations and veri ed their solutions in HOL Light.
We have already extended the reported formalization by formalizing the impedance force control and imagebased torque controller, which are mainly responsible for the process of cell injection [RH18]. In future, we plan to verify the relationship between both of these controllers. Another future direction is to formalize the 3-DOF motion stage and formally analyze the dynamics of the corresponding robotic cell injection system. [CGP99]
Edmund M Clarke, Orna Grumberg, and Doron Peled. Model Checking. MIT press, 1999. [CKNZ12] Edmund M Clarke, William Klieber, Milos Novacek, and Paolo Zuliani. Model Checking and the State Explosion Problem. In Tools for Practical Software Veri cation, volume 7682 of LNCS, pages 1{30. Springer, 2012.
Mohd Faroque and Sya zwan Nizam. Virtual Reality Training for Micro-robotic Cell Injection. Technical report, Deakin University, Australia, 2016.
John Harrison. HOL Light: A Tutorial Introduction. In Formal Methods in Computer-Aided Design, volume 1166 of LNCS, pages 265{269. Springer, 1996.
John Harrison. Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, 2009.
John Harrison. The HOL Light Theory of Euclidean Space. Journal of Automated Reasoning, pages 1{18, 2013.
HOL Light Multivariate Calculus.
Multivariate, 2018.
https://github.com/jrh13/hol-light/blob/master/ HOL Light Real Analysis. https://github.com/jrh13/hol-light/blob/master/Multivariate/ realanalysis.ml, 2018.
HOL Light Transcendental. https://github.com/jrh13/hol-light/blob/master/Multivariate/ transcendentals.ml, 2018. [HSM+09] Haibo Huang, Dong Sun, James K Mills, Wen J Li, and Shuk Han Cheng. Visual-based Impedance Control of Out-of-plane Cell Injection Systems. Transactions on Automation Science and Engineering, 6(3):565{571, 2009.
Osman Hasan and So ene Tahar. Formal Veri cation Methods. Encyclopedia of Information Science and Technology, IGI Global Pub, pages 7162{7170, 2015.
J Kuncova and Pasi Kallio. Challenges in Capillary Pressure Microinjection. In Engineering in Medicine and Biology Society, volume 2, pages 4998{5001. IEEE, 2004. Muhammad Usama Sardar and Osman Hasan. Towards Probabilistic Formal Modeling of Robotic Cell Injection Systems. In Models for Formal Analysis of Real Systems, pages 271{282, 2017.