Towards Probabilistic Formal Modeling of Robotic Cell Injection Systems
This work addresses the need for more reliable and rigorous analysis in robotic cell injection systems, which are critical for applications like gene injection and IVF, but it appears incremental as it applies an existing formal method to a specific domain problem.
The paper tackled the problem of analyzing force control algorithms in automated robotic cell injection systems, which are prone to failure due to uncertainties and non-exhaustive simulations, by presenting a formal analysis methodology based on probabilistic model checking that identified a discrepancy in the algorithm not found by traditional methods.
Cell injection is a technique in the domain of biological cell micro-manipulation for the delivery of small volumes of samples into the suspended or adherent cells. It has been widely applied in various areas, such as gene injection, in-vitro fertilization (IVF), intracytoplasmic sperm injection (ISCI) and drug development. However, the existing manual and semi-automated cell injection systems require lengthy training and suffer from high probability of contamination and low success rate. In the recently introduced fully automated cell injection systems, the injection force plays a vital role in the success of the process since even a tiny excessive force can destroy the membrane or tissue of the biological cell. Traditionally, the force control algorithms are analyzed using simulation, which is inherently non-exhaustive and incomplete in terms of detecting system failures. Moreover, the uncertainties in the system are generally ignored in the analysis. To overcome these limitations, we present a formal analysis methodology based on probabilistic model checking to analyze a robotic cell injection system utilizing the impedance force control algorithm. The proposed methodology, developed using the PRISM model checker, allowed to find a discrepancy in the algorithm, which was not found by any of the previous analysis using the traditional methods.