Surgical Robots: Behaviors Specification and reasoning

A Surgical robotic system is a computer assisted electromechanical device in a surgical context which helps the surgeon by performing interventions. This system is a safety critical system where occurring of errors might lead to the endangerment of human life, or substantial economic loss. Therefore, methods that guarantee the correctness of the system adherence to crucial safety properties are needed. A quite new way that can be used to specify the dynamics behaviors of surgical robots is to use hybrid automata. The semantics of hybrid automata allows us to reason about and to simulate the behavior of robots. This paper shows how to use hybrid automata to model a case study on the coordination between surgical robots working in a shareable area. Additionally the paper shows some formal analysis of particular requirements on both simulation and model checking level to reason about the behavior of the robots.