Formal Analysis of Robotic Cell Injection Systems using Theorem Proving

Abstract

Cell injection is an approach used for the delivery of small sample substances into a biological cell and is widely used in drug development, gene injection, intracytoplasmic sperm injection (ICSI) and in-virto fertilization (IVF). Robotic cell injection systems provide the automation of the process as opposed to the manual and semi-automated cell injection systems, which require expert operators and involve time consuming processes and also have lower success rates. The automation of the cell injection process is achieved by controlling the injection force and planning the motion of the injection pipette. Traditionally, these systems are analyzed using paper-and-pencil proof and computer simulation methods. However, the former is human-error prone and the later is based on the numerical algorithms, where the approximation of the mathematical expressions introduces inaccuracies in the analysis. Formal methods can overcome these limitations and thus provide an accurate analysis of the cell injection systems. Model checking, i.e., a state-based formal method, has been recently proposed for the analysis of these systems. However, it involves the discretization of the differential equations that are used for modeling the dynamics of the system and thus compromises on the completeness of the analysis of these safety-critical systems. In this project, we propose to use higher-order-logic theorem proving, a deductive-reasoning based formal method, for the modeling and analysis of the dynamical behaviour of the robotic cell injection systems.

Framework

People

Students

Professors

Publications

  1. A. Rashid and O. Hasan (2020). “Formal Verification of Robotic Cell Injection Systems upto 4-DOF using HOL Light”, Formal Aspects of Computing, Springer, Volume 32, No. 2-3, pp: 229-250, DOI: 10.1007/s00165-020-00514-3.
  2. A. Rashid and O. Hasan (2018). “Formal Modeling of Robotic Cell Injection Systems in Higher-order Logic”, Formal Verification of Physical Systems (FVPS), CICM Workshop, CEUR, pp: 1-9, Hagenberg, Austria.
  3. A. Rashid and O. Hasan (2017). “Formal Analysis of Robotic Cell Injection Systems using Theorem Proving”, Design, Modeling and Evaluation of Cyber Physical Systems (CyPhy), Lecture Notes in Computer Science (LNCS), Springer, Vol. 11267, pp: 127-141, Seoul, South Korea.