Abstract:
In biological cell micro-manipulation, small volumes of samples are injected
into suspended or adherent cells using cell injection procedures. It is extensively used for gene injection, in-vitro fertilization (IVF), intracytoplasmic
sperm injection (ISCI) and drug development procedures. Commonly used
approaches of manual or semi-automated techniques require extensive manual training and still have a high probability of contamination and low success
rate. Recently, fully automated cell injection systems have been proposed to
overcome these limitations. The overall success of the procedure in fully automated cell injection system mainly relies on accurate path planning of the
injection pipette and the amount of the injection forces applied at the time of
cell injection, using robotic controls. An inaccurate planning may lead to cell
rupture and failure of the overall procedure. Traditionally, fully automated
systems are analyzed and tested using simulation, which is inherently nonexhaustive and incomplete in terms of finding potential system failures. To
overcome these limitations, we present a probabilistic formal analysis based
on model checking approach to analyze fully automated robotic cell injection
systems based on their path planning and force control. For illustration, we present the formal analysis of a robotic cell injection system for out-of-plane
cell injection procedures where the proposed model has a very low probability of error in force control and position measurements with respect to its
desired counter parts. The success rate of the model is very high as chances
of poor or failed injection and cell rupture are very slim
