Top

Innovations in Systems and Software Engineering

Published in:

18-05-2018 | S.I. : VECOS2017

Formal probabilistic analysis of a surgical robot control algorithm with different virtual fixtures

Authors: Muhammad Saad Ayub, Osman Hasan

Published in: Innovations in Systems and Software Engineering | Issue 2/2018

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

Surgical robots are increasingly being used in operation theaters involving normal or laparoscopic surgeries. The working of these surgical robots is highly dependent on their control algorithms, which require very rigorous analysis to ensure their correct functionality due to the safety-critical nature of surgeries. Traditionally, safety of control algorithms is ensured by simulations, but they provide incomplete and approximate analysis results due to their inherent sampling-based nature. We propose to use probabilistic model checking, which is a formal verification method, for quantitative analysis, to verify the control algorithms of surgical robots in this paper. As an illustrative example, the paper provides a formal analysis of a virtual fixture control algorithm, implemented in a neuro-surgical robot, using the PRISM model checker. In particular, we provide a formal discrete-time Markov chain-based model of the given control algorithm and its environment. This formal model is then analyzed for multiple virtual fixtures, like cubic, hexagonal and irregular shapes. This verification allowed us to discover new insights about the considered algorithm that allow us to design safer control algorithms.

previous article Introduction to special issue on verification and evaluation of computer systems

next article Maximal software execution time: a regression-based approach

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Alur R, Courcoubetis C, Henzinger TA, Ho PH (1993) Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In: Hybrid systems, Springer, Berlin, pp 209–229

Alur R, Henzinger TA (1999) Reactive modules. Formal Methods Syst Des 15(1):7–48CrossRef

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 (VECoS), pp 1–16

Baier C, Katoen JP (2008) Principles of model checking. MIT Press, CambridgeMATH

Bebek O, Cavusoglu MC (2007) Intelligent control algorithms for robotic-assisted beating heart surgery. IEEE Trans Robot 23(3):468–480CrossRef

Bresolin D, Guglielmo LD, Geretti L, Muradore R, Fiorini P, Villa T (2012) Open problems in verification and refinement of autonomous robotic systems. In: Euromicro conference on digital system design, pp 469–476

Fainekos GE, Gazit HK, Pappas GJ (2005) Temporal logic motion planning for mobile robots. In: Robotics and automation, pp 2020–2025

Grinstead CM, Snell JL (1997) Introduction to probability. American Mathematical Soc, ProvidenceMATH

Groote JF, Mateescu R (1999) Verification of temporal properties of processes in a setting with data. In: Algebraic methodology and software technology (AMAST), pp 74–90

10.

Groote JF, Mathijssen A, Reniers M, Usenko Y, Weerdenburg MV (2007) The formal specification language mCRL2. Citeseer, University ParkMATH

11.

Hahn EM, Hermanns H, Wachter B, Zhang L (2009) Infamy: an infinite-state Markov model checker. In: Computer aided verification, pp 641–647

12.

Hahn EM, Hermanns H, Wachter B, Zhang L (2010) Param: a model checker for parametric Markov models. In: Computer aided verification, pp 660–664

13.

Hahn EM, Hermanns H, Wachter B, Zhang L (2010) Pass: abstraction refinement for infinite probabilistic models. In: Tools and algorithms for the construction and analysis of systems, pp 353–357

14.

Haidegger T, Benyó B, Kovács L, Benyó Z (2009) Force sensing and force control for surgical robots. In: Symposium on modeling and control in biomedical systems, pp. 401–406

15.

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

16.

Hasan O, Tahar S (2014) Formal verification methods. Encyclopedia of information science and technology. IGI Global, Hershey, pp 7162–7170

17.

Hassan T, Hameed A, Nasir S, Kamal N, Hasan O (2016) Al-zahrawi: a telesurgical robotic system for minimal invasive surgery. IEEE Syst J 10(3):1035–1045CrossRef

18.

Jeannet B, Argenio PD, Larsen K (2002) Rapture: A tool for verifying Markov decision processes. In: Concurrency theory (CONCUR), p 149

19.

Jeannet B, DArgenio P, Larsen K (2010) Fortuna: model checking priced probabilistic timed automata. In: Quantitative evaluation of systems, pp 273–281

20.

Kazanzides P, Zuhars J, Mittelstadt B, Taylor RH (1992) Force sensing and control for a surgical robot. In: Robotics and automation, pp 612–617

21.

Kim M, Kang KC, Lee H (2005) Formal verification of robot movements-a case study on home service robot shr100. In: Robotics and automation, pp 4739–4744

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

23.

Kwiatkowska M, Norman G, Parker D (2011) PRISM 4.0: verification of probabilistic real-time systems. In: Computer aided verification, pp 585–591

24.

Lahijanian M, Wasniewski J, Andersson SB, Belta C (2010) Motion planning and control from temporal logic specifications with probabilistic satisfaction guarantees. In: Robotics and automation, pp 3227–3232

25.

Li L, Shi Z, Guan Y, Zhao C, Zhang J, Wei H (2014) Formal verification of a collision-free algorithm of dual-arm robot in hol4. In: Robotics and automation (ICRA), pp 1380–1385

26.

Mikaël L (2012) Formal verification of flexibility in swarm robotics. Thesis, Department of Computer Science, Universit libre de Bruxelles

27.

Norman G, Parker D (2014) Quantitative verification: formal guarantees for timeliness, reliability and performance. Technical report, The London Mathematical Society and the Smith Institute

28.

Oldenkamp HA (2007) Probabilistic model checking: a comparison of tools. Master’s thesis, University of Twente, Enschede, Netherlands

29.

Platzer A, Quesel JD (2008) Keymaera: a hybrid theorem prover for hybrid systems (system description). In: Automated reasoning, Springer, pp 171–178

30.

Rosenberg LB (1993) Virtual fixtures: perceptual tools for telerobotic manipulation. In: Virtual reality annual international symposium, pp 76–82

31.

Saberi AK, Groote JF, Keshishzadeh S (2013) Analysis of path planning algorithms: a formal verification-based approach. In: Robotics and automation ICRA, pp 232–239

32.

Scherer S, Lerda F, Clarke EM (2005) Model checking of robotic control systems. In: International symposium on artificial intelligence, robotics and automation in space (i-SAIRAS), pp 5–8

33.

Webster M, Dixon C, Fisher M, Salem M, Saunders J, Koay K, Dautenhahn K (2014) Formal verification of an autonomous personal robotic assistant. In: Papers from the AAAI spring symposium (FVHMS 2014) on formal verification and modeling in human–machine systems, pp 74–79

34.

Whitcomb L, Yoerger D, Singh H, Howland J (1999) Advances in underwater robot vehicles for deep ocean exploration: navigation, control, and survey operations. In: International symposium on robotics research navigation, control and survey operations, pp 346–353

35.

Wulf D, M, Doyen L, Raskin JF (2004) Almost ASAP semantics: from timed models to timed implementations. In: Hybrid systems: computation and control, Springer, pp 296–310

36.

Xia T, Baird C, Jallo G, Hayes K, Nakajima N, Hata N, Kazanzides P (2008) An integrated system for planning, navigation and robotic assistance for skull base surgery. J Med Robot Comput Assist Surg 4(4):321–330CrossRef

Title: Formal probabilistic analysis of a surgical robot control algorithm with different virtual fixtures
Authors: Muhammad Saad Ayub
Osman Hasan
Publication date: 18-05-2018
Publisher: Springer London
Published in: Innovations in Systems and Software Engineering / Issue 2/2018
Print ISSN: 1614-5046
Electronic ISSN: 1614-5054
DOI: https://doi.org/10.1007/s11334-018-0315-8

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Other articles of this Issue 2/2018

Introduction to special issue on verification and evaluation of computer systems

Maximal software execution time: a regression-based approach

FC-AMAT: factor-based C-AMAT analysis in memory system measurement

TT-BIP: using correct-by-design BIP approach for modelling real-time system with time-triggered paradigm

Premium Partner