Cell injection is a technique in the domain of biological cellmicro-manipulation for the delivery of small volumes of samples into thesuspended or adherent cells. It has been widely applied in various areas, suchas gene injection, in-vitro fertilization (IVF), intracytoplasmic sperminjection (ISCI) and drug development. However, the existing manual andsemi-automated cell injection systems require lengthy training and suffer fromhigh probability of contamination and low success rate. In the recentlyintroduced fully automated cell injection systems, the injection force plays avital role in the success of the process since even a tiny excessive force candestroy the membrane or tissue of the biological cell. Traditionally, the forcecontrol algorithms are analyzed using simulation, which is inherentlynon-exhaustive and incomplete in terms of detecting system failures. Moreover,the uncertainties in the system are generally ignored in the analysis. Toovercome these limitations, we present a formal analysis methodology based onprobabilistic model checking to analyze a robotic cell injection systemutilizing the impedance force control algorithm. The proposed methodology,developed using the PRISM model checker, allowed to find a discrepancy in thealgorithm, which was not found by any of the previous analysis using thetraditional methods.
展开▼
