{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:49:00Z","timestamp":1740098940144,"version":"3.37.3"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319661759"},{"type":"electronic","value":"9783319661766"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-66176-6_1","type":"book-chapter","created":{"date-parts":[[2017,8,14]],"date-time":"2017-08-14T00:13:02Z","timestamp":1502669582000},"page":"1-16","source":"Crossref","is-referenced-by-count":1,"title":["Formal Probabilistic Analysis of a Virtual Fixture Control Algorithm for a Surgical Robot"],"prefix":"10.1007","author":[{"given":"Muhammad Saad","family":"Ayub","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Osman","family":"Hasan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,8,15]]},"reference":[{"key":"1_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/3-540-57318-6_30","volume-title":"Hybrid Systems","author":"R Alur","year":"1993","unstructured":"Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.-H.: Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.) HS 1991-1992. LNCS, vol. 736, pp. 209\u2013229. Springer, Heidelberg (1993). doi: 10.1007\/3-540-57318-6_30"},{"issue":"1","key":"1_CR2","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1023\/A:1008739929481","volume":"15","author":"R Alur","year":"1999","unstructured":"Alur, R., Henzinger, T.A.: Reactive modules. Formal Methods Syst. Des. 15(1), 7\u201348 (1999)","journal-title":"Formal Methods Syst. Des."},{"key":"1_CR3","doi-asserted-by":"crossref","unstructured":"Bresolin, D., Guglielmo, L.D., Geretti, L., Muradore, R., Fiorini, P., Villa, T.: Open problems in verification and refinement of autonomous robotic systems. In: Euromicro Conference on Digital System Design, pp. 469\u2013476 (2012)","DOI":"10.1109\/DSD.2012.96"},{"key":"1_CR4","doi-asserted-by":"crossref","unstructured":"Fainekos, G.E., Gazit, H.K., Pappas, G.J.: Temporal logic motion planning for mobile robots. In: Robotics and Automation, pp. 2020\u20132025 (2005)","DOI":"10.1109\/ROBOT.2005.1570410"},{"key":"1_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/3-540-49253-4_8","volume-title":"Algebraic Methodology and Software Technology","author":"JF Groote","year":"1998","unstructured":"Groote, J.F., Mateescu, R.: Verification of temporal properties of processes in a setting with data. In: Haeberer, A.M. (ed.) AMAST 1999. LNCS, vol. 1548, pp. 74\u201390. Springer, Heidelberg (1998). doi: 10.1007\/3-540-49253-4_8"},{"key":"1_CR6","unstructured":"Groote, J.F., Mathijssen, A., Reniers, M., Usenko, Y., Weerdenburg, M.V.: The formal specification language mCRL2. Citeseer (2007)"},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"Haidegger, T., Beny\u00f3, B., Kov\u00e1cs, L., Beny\u00f3, Z.: Force sensing and force control for surgical robots. In: Symposium on Modeling and Control in Biomedical Systems, pp. 401\u2013406 (2009)","DOI":"10.3182\/20090812-3-DK-2006.0035"},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Hasan, O., Tahar, S.: Formal Verification Methods. In: Encyclopedia of Information Science and Technology, pp. 7162\u20137170. IGI Global (2014)","DOI":"10.4018\/978-1-4666-5888-2.ch705"},{"issue":"3","key":"1_CR9","doi-asserted-by":"crossref","first-page":"1035","DOI":"10.1109\/JSYST.2014.2331146","volume":"10","author":"T Hassan","year":"2016","unstructured":"Hassan, T., Hameed, A., Nasir, S., Kamal, N., Hasan, O.: Al-Zahrawi: a telesurgical robotic system for minimal invasive surgery. IEEE Syst. J. 10(3), 1035\u20131045 (2016)","journal-title":"IEEE Syst. J."},{"key":"1_CR10","doi-asserted-by":"crossref","unstructured":"Kazanzides, P., Zuhars, J., Mittelstadt, B., Taylor, R.H.: Force sensing and control for a surgical robot. In: Robotics and Automation, pp. 612\u2013617 (1992)","DOI":"10.1109\/ROBOT.1992.220224"},{"key":"1_CR11","unstructured":"Kim, M., Kang, K.C., Lee, H.: Formal verification of robot movements-a case study on home service robot SHR100. In: Robotics and Automation, pp. 4739\u20134744 (2005)"},{"key":"1_CR12","doi-asserted-by":"crossref","unstructured":"Kouskoulas, Y., Renshaw, D., Platzer, A., Kazanzides, P.: Certifying the safe design of a virtual fixture control algorithm for a surgical robot. In: Hybrid Systems: Computation and Control, pp. 263\u2013272 (2013)","DOI":"10.1145\/2461328.2461369"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Computer Aided Verification, pp. 585\u2013591 (2011)","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"1_CR14","doi-asserted-by":"crossref","unstructured":"Lahijanian, M., Wasniewski, J., Andersson, S.B., Belta, C.: Motion planning and control from temporal logic specifications with probabilistic satisfaction guarantees. In: Robotics and Automation, pp. 3227\u20133232 (2010)","DOI":"10.1109\/ROBOT.2010.5509686"},{"key":"1_CR15","doi-asserted-by":"crossref","unstructured":"Li, L., Shi, Z., Guan, Y., Zhao, C., Zhang, J., Wei, H.: Formal verification of a collision-free algorithm of dual-arm robot in HOL4. In: Robotics and Automation (ICRA), pp. 1380\u20131385 (2014)","DOI":"10.1109\/ICRA.2014.6907032"},{"issue":"5","key":"1_CR16","doi-asserted-by":"crossref","first-page":"568","DOI":"10.1001\/jama.285.5.568","volume":"285","author":"MJ Mack","year":"2001","unstructured":"Mack, M.J.: Minimally invasive and robotic surgery. J. Am. Med. Assoc. 285(5), 568\u2013572 (2001)","journal-title":"J. Am. Med. Assoc."},{"key":"1_CR17","unstructured":"Mika\u00ebl, L.: Formal verification of flexibility in swarm robotics. Thesis, Department of Computer Science, Universit libre de Bruxelles (2012)"},{"key":"1_CR18","unstructured":"Oldenkamp, H.A.: Probabilistic model checking: a comparison of tools. Master\u2019s thesis, University of Twente, Enschede, Netherlands (2007)"},{"key":"1_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-540-71070-7_15","volume-title":"Automated Reasoning","author":"A Platzer","year":"2008","unstructured":"Platzer, A., Quesel, J.-D.: KeYmaera: a hybrid theorem prover for hybrid systems (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS, vol. 5195, pp. 171\u2013178. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-71070-7_15"},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"Rosenberg, L.B.: Virtual fixtures: Perceptual tools for telerobotic manipulation. In: Virtual Reality Annual International Symposium, pp. 76\u201382 (1993)","DOI":"10.1109\/VRAIS.1993.380795"},{"key":"1_CR21","doi-asserted-by":"crossref","unstructured":"Saberi, A.K., Groote, J.F., Keshishzadeh, S.: Analysis of path planning algorithms: a formal verification-based approach. In: Robotics and Automation ICRA, pp. 232\u2013239 (2013)","DOI":"10.7551\/978-0-262-31709-2-ch035"},{"key":"1_CR22","unstructured":"Scherer, S., Lerda, F., Clarke, E.M.: Model checking of robotic control systems. In: International Symposium on Artificial Intelligence, Robotics and Automation in Space (i-SAIRAS), pp. 5\u20138 (2005)"},{"key":"1_CR23","unstructured":"Webster, M., Dixon, C., Fisher, M., Salem, M., Saunders, J., Koay, K., Dautenhahn, K.: Formal verification of an autonomous personal robotic assistant. In: Formal Verification and Modeling in Human-Machine Systems: Papers from the AAAI Spring Symposium (FVHMS 2014), pp. 74\u201379 (2014)"},{"issue":"4","key":"1_CR24","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1002\/rcs.213","volume":"4","author":"T Xia","year":"2008","unstructured":"Xia, T., Baird, C., Jallo, G., Hayes, K., Nakajima, N., Hata, N., Kazanzides, P.: An integrated system for planning, navigation and robotic assistance for skull base surgery. J. Med. Robot. Comput. Assist. Surg. 4(4), 321\u2013330 (2008)","journal-title":"J. Med. Robot. Comput. Assist. Surg."}],"container-title":["Lecture Notes in Computer Science","Verification and Evaluation of Computer and Communication Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66176-6_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,2]],"date-time":"2019-10-02T06:50:03Z","timestamp":1569999003000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66176-6_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319661759","9783319661766"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66176-6_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}