{'fraction_non_alphanumeric': 0.029778998626545136, 'fraction_numerical': 0.007803720814084155, 'mean_word_length': 4.915435745937962, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 1, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Formal Modeling of Robotic Cell Injection Systems in Higher-order Logic

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 paper-and-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 differential 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.


Introduction
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 insufficient 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 verification 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 differential equations that model the dynamics of these systems, which compromises the accuracy of the corresponding analysis. Moreover, the analysis also suffers from the inherent state-space explosion problem [CKNZ12]. Higher-order-logic theorem proving [Har09] is an interactive verification technique that can overcome these limitations. It primarily involves the mathematical modeling of the system based on higher-order logic and verification of its properties based on deductive reasoning. Given the high expressiveness of higher-order logic, it can truly capture the behavior of the differential 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 verification 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 differential equations and the formal verification 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.

Multivariable Calculus Theories in HOL Light
A N-dimensional vector in HOL Light is modeled as a R N 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 verified for functions with an arbitrary data-type We explain some of the frequently used HOL Light functions in the proposed formalization as follows: Definition 2.1. Vector ∀ 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 n th element of a list L. Here, the lambda operator in HOL is used for constructing a vector based on its components [Har13].
Definition 2.2. Real Cosine and Real Sine ∀ x. cos x = Re (ccos (Cx x)) ∀ 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 : R 2 → R 2 and complex sine csin : R 2 → R 2 functions, respectively.
The function real derivative represents the derivative of a real-valued function and is defined 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 differentiated, and returns a variable of data-type R, which is the differential of f at x. The function has real derivative defines 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.

Robotic Cell Injection Systems
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 configuration of a robotic cell injection system is depicted in Figure 2. The stage (table and working

Formal Modeling of Robotic Cell Injection System
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 find 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: 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 (o c − x x y c z c ), and the rotation matrix from the stage coordinate frame to the camera coordinate frame as: The verification 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: 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 verification of their interrelationship: : two dim coordinates u v t = dis resol matrix fx fy * * two dim coordinates xc yc t ∧ [A6]: two dim coordinates xc yc t = rotat matrix alpha * * two dim coordinates x y t + displace vector dx dy ⇒ two dim coordinates u v t = transfor matrix fx fy alpha * * two dim coordinates x y t + fx * dx fy * 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 verification 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: where m x , m y and m p represent the masses of the xy positioning tables and working plate, respectively. Similarly, f ex d and f ey d 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)  where mass matrix is the matrix containing the respective masses, i.e., m x , m y and m p , 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 first-order and second-order derivatives of the stage coordinates, respectively: Definition 4.6. Vectors Containing First and Second-order Derivatives of the Stage Coordinates ∀ x y t. fir order deriv stage coordinates x y t = deriv vector first [x; y] t ∀ 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 first 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: We verify the solution of the above equation in HOL Light as the following theorem:  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 differentiability conditions for the image coordinate and their first-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 effort 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 verified theorems are universally quantified 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.

Conclusion
In this paper, we proposed formal modeling of robotic cell injection systems in higher-order logic. We first formalized the camera, image and stage coordinate frames, which are the vital components of a robotic cell injection system, and formally verified their interrelationship using the HOL Light proof assistant. We also formalized the dynamical behaviour of the 2-DOF motion stage based on differential equations and verified 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.