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.


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Formal Verification Applied to Robotic Surgery


    Additional title:

    Lect. Notes Control


    Contributors:


    Publication date :

    2014-09-26


    Size :

    9 pages





    Type of media :

    Article/Chapter (Book)


    Type of material :

    Electronic Resource


    Language :

    English




    FORMAL VERIFICATION APPLIED TO SPACECRAFT ATTITUDE CONTROL

    Lang, Kendra / Klett, Corbin / Hawkins, Kelsey et al. | TIBKAT | 2021


    Formal Verification Applied to Spacecraft Attitude Control

    Lang, Kendra / Klett, Corbin / Hawkins, Kelsey et al. | AIAA | 2021


    Formal verification and legacy redesign

    Young, F.C.D. / Houston, J.A. | IEEE | 1999


    Formal verification and legacy redesign

    Young, F.C.D. / Houston, J.A. | IEEE | 1998


    Formal Verification at System Level

    Mazzini, S. / Puri, S. / Mari, F. et al. | British Library Conference Proceedings | 2009