Formal verification of robotic cell injection systems up to 4-DOF using \textsf{HOL Light}

DOI10.1007/S00165-020-00514-3MaRDI QIDQ2198134zbMATH OpenOpenAlexWikidataFDO

Authors Adnan Rashid, Osman Hasan

Publication date 9 September 2020

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1805.02858

zbMATH Keywords

formal verificationhigher-order logicHOL Lightrobotic cell injection systemstheorem proving

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Artificial intelligence for robotics (68T40) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

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 paper, 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. The proposed analysis, based on the HOL Light theorem prover, enabled us to identify some discrepancies in the simulation and model checking based analysis of the same robotic cell injection system.

Recommendations

• Formal Verification Applied to Robotic Surgery
• Task level specification and formal verification of robotics control systems: State of the art and case study
• Formal analysis of optical systems
• Modelling and Verification of Timed Robotic Controllers
• Formal verification of stability and chaos in periodic optical systems

Cites work

• scientific article; zbMATH DE number 5539366 (Why is no real title available?)
• scientific article; zbMATH DE number 958048 (Why is no real title available?)
• Model checking
• Model checking of probabilistic and nondeterministic systems
• The HOL Light theory of Euclidean space
• The misfortunes of a trio of mathematicians using computer algebra systems. Can we trust in them?

Cited in

(2)

• Formalization of the inverse kinematics of three-fingered dexterous hand
• Formalization of robot collision detection method based on conformal geometric algebra

Describes a project that uses

Uses Software

• transcendentals.ml
• Mathematica
• ML
• HOL
• Matlab
• HOL Light
• Maple
• Robotica
• GitHub

This page was built for publication: Formal verification of robotic cell injection systems up to 4-DOF using \textsf{HOL Light}

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2198134)