迈向机器人细胞注射系统的概率形式化建模

细胞注射是生物细胞微操作领域的一项技术，用于向悬浮或贴壁细胞递送小体积样品。它已广泛应用于各个领域，如基因注射、体外受精(IVF)、卵胞浆内单精子注射(ISCI)和药物开发。然而，现有的手动和半自动细胞注射系统需要冗长的培训，并且具有高污染概率和低成功率。在最近引入的全自动细胞注射系统中，注射力在过程成功中起着至关重要的作用，因为即使微小的过大力量也会破坏生物细胞的膜或组织。传统上，力控制算法使用仿真分析，这在检测系统故障方面天生非穷举且不完备。此外，系统中的不确定性通常在分析中被忽略。为克服这些限制，我们提出一种基于概率模型检测的形式化分析方法，利用阻抗力控制算法分析机器人细胞注射系统。所提出的方法使用PRISM模型检查器开发，能够发现算法中的差异，这是之前使用传统方法的任何分析都未发现的。