×

Formal verification applied to robotic surgery. (English) Zbl 1403.93140

van Schuppen, Jan H. (ed.) et al., Coordination control of distributed systems. Cham: Springer (ISBN 978-3-319-10406-5/pbk; 978-3-319-10407-2/ebook). Lecture Notes in Control and Information Sciences 456, 347-355 (2015).
Summary: 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.
For the entire collection see [Zbl 1310.93004].

MSC:

93C85 Automated systems (robots, etc.) in control theory
93B03 Attainable sets, reachability
90B25 Reliability, availability, maintenance, inspection in operations research
68Q45 Formal languages and automata
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] 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
[2] Alur R, Dang T, Ivančić F (2006) Counterexample-guided predicate abstraction of hybrid systems. Theor Comput Sci 354(2):250-271 · Zbl 1088.68096 · doi:10.1016/j.tcs.2005.11.026
[3] 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 · Zbl 1284.93121
[4] Frehse G (2008) PHAVer: algorithmic verification of hybrid systems past HyTech. Int J Softw Tools Technol Transfer (STTT) 10:263-279 · doi:10.1007/s10009-007-0062-x
[5] 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
[6] 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 · doi:10.1109/MRA.2011.942112
[7] Ratschan S, She Z (2007) Safety verification of hybrid systems by constraint propagation based abstraction refinement. ACM Trans Embed Comput Syst 6(1):8 · Zbl 1078.93508
[8] Siciliano B, Sciavicco L, Villani L, Oriolo G (2008) Robotics: modelling, planning and control. Springer, Berlin
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.