Abstract
In this essay, 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 preoperative 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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Alur R, Courcoubetis C, Henzinger TA, Ho PH (1992) Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In: Hybrid systems, LNCS, vol 736. Springer, Berlin, pp 209–229
Alur R, Dang T, Ivančić F (2006) Counterexample-guided predicate abstraction of hybrid systems. Theor Comput Sci 354(2):250–271
Benvenuti L, Bresolin D, Collins P, Ferrari A, Geretti L, Villa T (2014) Assume-guarantee verification of nonlinear hybrid systems with ARIADNE. Int J Robust Nonlinear Control 24:699–724
Frehse G (2008) PHAVer: algorithmic verification of hybrid systems past HyTech. Int J Softw Tools Technol Transfer (STTT) 10:263–279
Frehse G, Le Guernic C, Donzé A, Cotton S, Ray R, Lebeltel O, Ripado R, Girard A, Dang T, Maler O (2011) SpaceEx: scalable verification of hybrid systems. In: Proceddings of 23rd international conference on computer aided verification (CAV 2011), LNCS, vol 6806. Springer, Berlin/Heidelberg, pp 379–395
Muradore R, Bresolin D, Geretti L, Fiorini P, Villa T (2011) Robotic surgery: formal verification of plans. Robot Autom Mag IEEE 18(3):24–32
Ratschan S, She Z (2007) Safety verification of hybrid systems by constraint propagation based abstraction refinement. ACM Trans Embed Comput Syst 6(1):8
Siciliano B, Sciavicco L, Villani L, Oriolo G (2008) Robotics: modelling, planning and control. Springer, Berlin
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this chapter
Cite this chapter
Bresolin, D., Geretti, L., Muradore, R., Fiorini, P., Villa, T. (2015). Formal Verification Applied to Robotic Surgery. In: van Schuppen, J., Villa, T. (eds) Coordination Control of Distributed Systems. Lecture Notes in Control and Information Sciences, vol 456. Springer, Cham. https://doi.org/10.1007/978-3-319-10407-2_40
Download citation
DOI: https://doi.org/10.1007/978-3-319-10407-2_40
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-10406-5
Online ISBN: 978-3-319-10407-2
eBook Packages: EngineeringEngineering (R0)