Formal Analysis of Robotic Cell Injection Systems using Theorem Proving

Abstract

Cell injection delivers small sample substances into a biological cell, and is widely used in drug development, gene injection, intracytoplasmic sperm injection (ICSI), and in-vitro fertilization (IVF). Robotic cell injection systems automate this process, controlling injection force and planning pipette motion — but manual and semi-automated systems require expert operators, are time-consuming, and have lower success rates.

Traditionally these systems are analyzed with paper-and-pencil proofs (human-error-prone) or computer simulation (numerical approximation introduces inaccuracy). Model checking has recently been proposed, but requires discretizing the governing differential equations, compromising completeness. We propose higher-order-logic theorem proving — a deductive-reasoning-based formal method — for modeling and analyzing the dynamical behavior of robotic cell injection systems, up to 4 degrees of freedom.

People