More Web Proxy on the site http://driver.im/

research-article

Open access

Formal Verification of Robotic Cell Injection systems up to 4-DOF using HOL Light

Authors:

Osman HasanAuthors Info & Claims

Formal Aspects of Computing, Volume 32, Issue 2-3

Pages 229 - 250

https://doi.org/10.1007/s00165-020-00514-3

Published: 01 July 2020 Publication History

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 and in-vitro fertilization. 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 obtained by controlling the orientation and movement of its various components, like injection manipulator, microscope etc., and planning the motion of the injection pipette by controlling the force of the injection. The conventional techniques to analyze the cell injection process include paper-and-pencil proof and computer simulation methods. However, both these techniques suffer from their inherent limitations, such as, proneness to human error for the former and the approximation of the mathematical expressions involved in the numerical algorithms for the latter. Formal methods have the capability to overcome these limitations and can provide an accurate analysis of these cell injection systems. Model checking, i.e., a state-based formal method, has been recently used for analyzing these systems. However, it involves the discretization of the differential equations capturing the continuous dynamics of the system and thus compromises on the completeness of the analysis of these safety-critical systems. In this paper, we propose a higher-order-logic theorem proving (a deductive-reasoning based formal method) based framework for analyzing the dynamical behavior of the robotic cell injection systems upto 4-DOF. 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.

References

References

[1]

Ayub MS, Hasan O (2017) Formal probabilistic analysis of a virtual fixture control algorithm for a surgical robot. In: Verification and evaluation of computer and communication systems, volume 10466 of LNCS, pp 1–16. Springer

[2]

Bianco A, De Alfaro L (1995) Model checking of probabilistic and nondeterministic systems. I:n Foundations of software technology and theoretical computer science, volume 1026 of LNCS, pp 499–513. Springer

[3]

Bresolin D, Geretti L, Muradore R, Fiorini P, and Villa T Formal verification of robotic surgery tasks by reachability analysis Microprocess Microsyst 2015 39 8 836-842

Digital Library

[4]

Clarke, E.M., Grumberg, O., Peled, D.: Model checking. MIT Press (1999)

[5]

Clarke EM, Klieber W, Nováček M, Zuliani P (2012) Model checking and the state explosion problem. In: Tools for practical software verification, volume 7682 of LNCS, pp 1–30. Springer

[6]

Dawood H (2011) Theories of interval arithmetic: mathematical foundations and applications. LAP Lambert Academic Publishing

[7]

Durán AJ, Pérez M, Varona JL (2013) The misfortunes of a mathematicians' Trio using computer algebra systems: can we trust? CoRR. arXiv:1312.3270

[8]

Faroque M, Nizam S (2016) Virtual reality training for micro-robotic cell injection. Technical report, Deakin University, Australia

[9]

Gordon Michael JC (1988) HOL: a proof generating system for higher-order logic. In: VLSI specification, verification and synthesis, volume 35 of SECS, pp 73–128. Springer

[10]

Harrison J (1996) HOL light: a tutorial introduction. In: Srivas M, Camilleri A (eds) Proceedings of the first international conference on formal methods in computer-aided design (FMCAD'96), volume 1166 of LNCS, pp 265–269. Springer-Verlag

[11]

Harrison J (1996) HOL light: a tutorial introduction. In: Formal methods in computer-aided design, volume 1166 of LNCS, pp 265–269. Springer

[12]

Harrison, J.: Handbook of practical logic and automated reasoning. Cambridge University Press (2009)

[13]

Harrison J(2013) The HOL light theory of euclidean space. J Autom Reason 1–18

[14]

HOL Light Multivariate Calculus (2020) https://github.com/jrh13/hol-light/blob/master/Multivariate

[15]

HOL Light Real Calculus (2020) https://github.com/jrh13/hol-light/blob/master/Multivariate/realanalysis.ml

[16]

HOL Light Transcendentals (2020) https://github.com/jrh13/hol-light/blob/master/Multivariate/transcendentals.ml

[17]

HOL Light Vectors and Matrices (2020) https://github.com/jrh13/hol-light/blob/master/Multivariate/vectors.ml

[18]

Huang H, Sun D, Mills JK, Li WJ, and Cheng SH Visual-based impedance control of out-of-plane cell injection systems Trans Autom Sci Eng 2009 6 3 565-571

[19]

Huang H, Sun D, Mills JK, Li Wen J (2006) A visual impedance force control of a robotic cell injection system. In: Robotics and biomimetics, pp 233–238. IEEE

[20]

Hasan O, Tahar S (2015) Formal verification methods. In: Encyclopedia of information science and technology, pp 7162–7170. IGI Global Pub

[21]

Kuncova J, Kallio Pasi (2004) Challenges in capillary pressure microinjection. In: Engineering in Medicine and Biology Society, volume 2, pp 4998–5001. IEEE

[22]

Kouskoulas Y, Renshaw D, Platzer A, Kazanzides P (2013) Certifying the safe design of a virtual fixture control algorithm for a surgical robot. In: Hybrid systems: computation and control, pp 263–272. ACM

[23]

Maple (2020) https://www.maplesoft.com/

[24]

Mathematica (2020) https://www.wolfram.com/mathematica/

[25]

Nakayama T, Fujiwara H, Tastumi K, Fujita K, Higuchi T, and Mori T A new assisted hatching technique using a piezo-micromanipulator Fertil Steril 1998 69 4 784-788

[26]

Nethery JF and Spong MW Robotica: a mathematica package for robot analysis IEEE Robot Autom Mag 1994 1 1 13-20

[27]

Paulson, L.C.: ML for the working programmer. Cambridge University Press (1996)

[28]

Rashid A (2020) Formal verification of robotic cell injection systems upto

4

-DOF using HOL Light. http://save.seecs.nust.edu.pk/fvrcis/

[29]

Rashid A, Hasan O (2017) Formal analysis of robotic cell injection systems using theorem proving. In: Design, modeling, and evaluation of cyber physical systems, volume 11267 of LNCS, pp 127–141. Springer

[30]

Rashid A, Hasan O (2018) Formal modeling of robotic cell injection systems in higher-order logic. In: Formal verification of physical systems, volume 2307, pp 1–9. CEUR-WS

[31]

Sardar MU, Hasan O (2017) Towards probabilistic formal modeling of robotic cell injection systems. In: Models for formal analysis of real systems, pp 271–282

[32]

Sun D, Liu Y (1997) Modeling and impedance control of a two-manipulator system handling a flexible beam. In: Proceedings of 1997 IEEE International Conference on Robotics and automation, volume 2, pp 1787–1792. IEEE

[33]

Sun Y and Nelson BJ Biological cell injection using an autonomous microrobotic system Robot Res 2002 21 10–11 861-868

Digital Library

[34]

Yanagida K, Katayose H, Yazawa H, Kimura Y, Konnai K, and Sato A The usefulness of a piezo-micromanipulator in intracytoplasmic sperm injection in humans Hum Reprod 1999 14 2 448-453

Cited By

Aksoy KRashid ATahar S(2024)Formal Kinematic Analysis of Epicyclic Bevel Gear TrainsFormal Methods and Software Engineering10.1007/978-981-96-0617-7_10(162-180)Online publication date: 2-Dec-2024
https://dl.acm.org/doi/10.1007/978-981-96-0617-7_10
Wang GChen SGuan YShi ZLi XZhang J(2023)Formalization of the inverse kinematics of three-fingered dexterous handJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2023.100861133(100861)Online publication date: Jun-2023
https://doi.org/10.1016/j.jlamp.2023.100861
Qasim URashid AHasan O(2022)Formalization of bond graph using higher-order-logic theorem provingISA Transactions10.1016/j.isatra.2021.11.042128(453-469)Online publication date: Sep-2022
https://doi.org/10.1016/j.isatra.2021.11.042
Show More Cited By

Recommendations

Formalizing Potential Flows Using the HOL Light Theorem Prover
Formal Methods and Software Engineering
Abstract
Potential flow is a theoretical model that describes the movement of a fluid, e.g., water or air in situations where viscosity and turbulence are assumed to be negligible. This type of flow is often used as an idealized model to describe the ...
Mechanising Gödel–Löb Provability Logic in HOL Light
Abstract
We introduce our implementation in HOL Light of the metatheory for Gödel–Löb provability logic (GL), covering soundness and completeness w.r.t. possible world semantics and featuring a prototype of a theorem prover for GL itself. The strategy we ...
A Formalization and Proof Checker for Isabelle’s Metalogic
Abstract
Isabelle is a generic theorem prover with a fragment of higher-order logic as a metalogic for defining object logics. Isabelle also provides proof terms. We formalize this metalogic and the language of proof terms in Isabelle/HOL, define an ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Formal Aspects of Computing

Formal Aspects of Computing Volume 32, Issue 2-3

Jul 2020

203 pages

ISSN:0934-5043

EISSN:1433-299X

Issue’s Table of Contents

© British Computer Society 2020.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 July 2020

Accepted: 05 May 2020

Received: 29 April 2019

Published in FAC Volume 32, Issue 2-3

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
82
Total Downloads

Downloads (Last 12 months)32
Downloads (Last 6 weeks)4

Reflects downloads up to 03 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Aksoy KRashid ATahar S(2024)Formal Kinematic Analysis of Epicyclic Bevel Gear TrainsFormal Methods and Software Engineering10.1007/978-981-96-0617-7_10(162-180)Online publication date: 2-Dec-2024
https://dl.acm.org/doi/10.1007/978-981-96-0617-7_10
Wang GChen SGuan YShi ZLi XZhang J(2023)Formalization of the inverse kinematics of three-fingered dexterous handJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2023.100861133(100861)Online publication date: Jun-2023
https://doi.org/10.1016/j.jlamp.2023.100861
Qasim URashid AHasan O(2022)Formalization of bond graph using higher-order-logic theorem provingISA Transactions10.1016/j.isatra.2021.11.042128(453-469)Online publication date: Sep-2022
https://doi.org/10.1016/j.isatra.2021.11.042
Dang SCao S(2021)Regulation-as-a-Service: Model Checking for Decision-Making Behaviors in Price-Sensitive Service Systems2021 IEEE International Conference on Services Computing (SCC)10.1109/SCC53864.2021.00012(1-12)Online publication date: Sep-2021
https://doi.org/10.1109/SCC53864.2021.00012
Dang SCao SLi JZhang X(2021)Dynamic incentive mechanism design for regulation‐aware systemsInternational Journal of Intelligent Systems10.1002/int.2267037:2(1299-1321)Online publication date: 28-Dec-2021
https://dl.acm.org/doi/10.1002/int.22670

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents