In this paper we discuss the application of formal methods for the verification of properties of control systems designed for autonomous robotic systems. We illustrate our proposal in the context of surgery by considering the automatic execution of a simple action such as puncturing. To prove that a sequence of subtasks planned on pre-operative data can successfully accomplish the surgical operation despite model uncertainties, we specify the problem by using hybrid automata. We express the requirements of interest as questions about reachability 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.
Davide Bresolin, Luca Geretti, Riccardo Muradore, Paolo Fiorini, Tiziano Villa (2014). Verification of Robotic Surgery Tasks by Reachability Analysis: A Comparison of Tools. IEEE [10.1109/DSD.2014.55].
Verification of Robotic Surgery Tasks by Reachability Analysis: A Comparison of Tools
BRESOLIN, DAVIDE;
2014
Abstract
In this paper we discuss the application of formal methods for the verification of properties of control systems designed for autonomous robotic systems. We illustrate our proposal in the context of surgery by considering the automatic execution of a simple action such as puncturing. To prove that a sequence of subtasks planned on pre-operative data can successfully accomplish the surgical operation despite model uncertainties, we specify the problem by using hybrid automata. We express the requirements of interest as questions about reachability 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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
