In this paper we discuss the application of formal methods for the verification of propertiesof control systems designed for autonomous robotic systems.We illustrate our proposal in the context of surgery by considering the automatic executionof a simple action such as puncturing.To prove that a sequence of subtasks planned on pre-operative datacan successfully accomplish the surgical operation despite modeluncertainties, we specify the problem by using hybrid automata.We express the requirements of interest as questions aboutreachability properties of the hybrid automaton model.Then, we compare the different performance of current state-of-the art tools for reachability analysis of hybrid automata.

Verification of Robotic Surgery Tasks by Reachability Analysis: a Comparison of Tools

BRESOLIN, Davide;GERETTI, Luca;MURADORE, Riccardo;FIORINI, Paolo;VILLA, Tiziano
2014-01-01

Abstract

In this paper we discuss the application of formal methods for the verification of propertiesof control systems designed for autonomous robotic systems.We illustrate our proposal in the context of surgery by considering the automatic executionof a simple action such as puncturing.To prove that a sequence of subtasks planned on pre-operative datacan successfully accomplish the surgical operation despite modeluncertainties, we specify the problem by using hybrid automata.We express the requirements of interest as questions aboutreachability properties of the hybrid automaton model.Then, we compare the different performance of current state-of-the art tools for reachability analysis of hybrid automata.
2014
hybrid systems modeling and verification; reachability analysis; robotic surgery
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/787450
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? 2
social impact