{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,6,10]],"date-time":"2023-06-10T08:26:39Z","timestamp":1686385599299},"reference-count":44,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2018,7,5]],"date-time":"2018-07-05T00:00:00Z","timestamp":1530748800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Cyber-Phys. Syst."],"published-print":{"date-parts":[[2018,10,31]]},"abstract":"\n The use of robots in operating rooms improves safety and decreases patient recovery time and surgeon fatigue, but it introduces new potential hazards that can lead to severe injury or even the loss of human life. Thus, safety has been perceived as a crucial system property since the early days by the industry, the medical community, and the regulatory agents. In this article, we discuss the application of the mathematically rigorous technique known as Formal Verification to analyze the safety properties of a laser incision case study, and we assess its safe and predictable operation. Like all formal methods approaches, our analysis has three distinct components: a method to create a model of the system, a language to specify the properties, and a strategy to prove rigorously that the behavior of the model fulfills the desired properties. The model of the system takes the form of a hybrid automaton consisting of a discrete control part that operates in a continuous environment. The safety constraints are formalized as reachability properties of the hybrid automaton model, while the verification strategy exploits the capabilities of the tool A\n riadne<\/jats:sc>\n to address the verification problem and answer the related questions ranging from safety to efficiency and effectiveness.\n <\/jats:p>","DOI":"10.1145\/3140237","type":"journal-article","created":{"date-parts":[[2018,7,5]],"date-time":"2018-07-05T19:19:10Z","timestamp":1530818350000},"page":"1-29","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Formal Verification of Medical CPS"],"prefix":"10.1145","volume":"2","author":[{"given":"Andr\u00e9 A.","family":"Geraldes","sequence":"first","affiliation":[{"name":"University of Verona, Italy, and Istituto Italiano di Tecnologia, Verona, Italy"}]},{"given":"Luca","family":"Geretti","sequence":"additional","affiliation":[{"name":"University of Verona, Verona, Italy"}]},{"given":"Davide","family":"Bresolin","sequence":"additional","affiliation":[{"name":"University of Padova, Padova, Italy"}]},{"given":"Riccardo","family":"Muradore","sequence":"additional","affiliation":[{"name":"University of Verona, Verona, Italy"}]},{"given":"Paolo","family":"Fiorini","sequence":"additional","affiliation":[{"name":"University of Verona, Verona, Italy"}]},{"given":"Leonardo S.","family":"Mattos","sequence":"additional","affiliation":[{"name":"Istituto Italiano di Tecnologia, Via Morego, Genova, Italy"}]},{"given":"Tiziano","family":"Villa","sequence":"additional","affiliation":[{"name":"University of Verona, Verona, Italy"}]}],"member":"320","published-online":{"date-parts":[[2018,7,5]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2038642.2038685"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00202-T"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-40903-8_6"},{"key":"e_1_2_1_5_1","volume-title":"Medical robots: Current systems and research directions. J. Robot","author":"Beasley Ryan A.","year":"2012"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1002\/spe.1006"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1002\/rnc.2914"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1177\/0278364909104276"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSD.2014.55"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.micpro.2015.10.006"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2012.70"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_18"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_4"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.3109\/10929080109146301"},{"key":"e_1_2_1_15_1","volume-title":"A Discussion of Safety Issues for Medical Robots","author":"Davies Brian L."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1177\/0278364909338986"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0951-8320(01)00037-0"},{"key":"e_1_2_1_18_1","volume-title":"Cognitive Supervision for Robot-Assisted Minimally Invasive Laser Surgery","author":"Fichera Loris","edition":"1"},{"key":"e_1_2_1_19_1","first-page":"1","article-title":"Online estimation of laser incision depth for transoral microsurgery: Approach and preliminary evaluation","volume":"12","author":"Fichera Loris","year":"2015","journal-title":"Int. J. Med. Robot. Comput. Assist. Surg."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/3220883.3220991"},{"key":"e_1_2_1_21_1","volume-title":"Proceedings of the 23rd International Conference on Computer Aided Verification (CAV\u201911)","volume":"6806","author":"Frehse G."},{"key":"e_1_2_1_22_1","volume-title":"Proceedings of the International Conference on Automated Deduction (CADE\u201915)","volume":"9195","author":"Fulton N."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/TRO.2009.2022552"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/788018.788803"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1998.1581"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/11813040_1"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTCSA.2010.42"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2006.113"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.conengprac.2006.07.005"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/MRA.2008.926390"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2038642.2038667"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2461328.2461369"},{"key":"e_1_2_1_33_1","first-page":"3","article-title":"Robot challenges: Toward development of verification and synthesis techniques {from the Guest Editors}","volume":"18","author":"Kress-Gazit H.","year":"2011","journal-title":"IEEE Robot. Autom. Mag."},{"key":"e_1_2_1_34_1","first-page":"1","article-title":"Challenges and research directions in medical cyber--physical systems","volume":"100","author":"Lee I.","year":"2012","journal-title":"Proc. IEEE"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.cursur.2004.03.009"},{"key":"e_1_2_1_36_1","first-page":"27","article-title":"Roadmap for medical and healthcare robotics. In A Roadmap for U.S. Robotics\u2014From Internet to Robotics (2013 ed.). Georgia Institute of Technology, Atlanta, GA","volume":"2","author":"Matari\u0107 Maja","year":"2013","journal-title":"Chapter"},{"key":"e_1_2_1_37_1","volume-title":"Proceedings of the IEEE\/RSJ International Conference on Intelligent Robots and Systems. IEEE, 1359--1365","author":"Mattos L. S."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/MRA.2011.942112"},{"key":"e_1_2_1_39_1","volume-title":"Laser-tissue Interactions. Fundamentals and Applications","author":"Niemz Markolf H."},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2015.2453253"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1210268.1210276"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2006.890107"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2006.880669"},{"key":"e_1_2_1_44_1","volume-title":"Proceedings of the 5th International Conference on Advanced Robotics (ICAR\u201991)","volume":"1","author":"Taylor R. H."}],"container-title":["ACM Transactions on Cyber-Physical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3140237","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,31]],"date-time":"2022-12-31T22:05:03Z","timestamp":1672524303000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3140237"}},"subtitle":["A Laser Incision Case Study"],"short-title":[],"issued":{"date-parts":[[2018,7,5]]},"references-count":44,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2018,10,31]]}},"alternative-id":["10.1145\/3140237"],"URL":"https:\/\/doi.org\/10.1145\/3140237","relation":{},"ISSN":["2378-962X","2378-9638"],"issn-type":[{"value":"2378-962X","type":"print"},{"value":"2378-9638","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,7,5]]},"assertion":[{"value":"2016-08-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-09-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-07-05","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}