Formal Analysis Of A Micro-robotic Cell Injection System Using Probabilistic Model Checking

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