Surgical robotics system is an area which received attention in the area of robotics. A robotic Surgery is de ned as a computer assisted electro-mechanical device in a surgical environment which supports the surgeon by performing interventions. One of the most famous surgical robotic systems is the da Vinci system which is used for minimally invasive robotic Surgery. The da Vinci consists of up to three robotic arms for holding surgical equipment's, a patient side cart including one robotic arm equipped with an endoscopic camera. Generally, Surgical robotic systems are consider safety critical systems where occurring of errors might lead to the risk of human life, to economic loss, or to a huge environment danger. Therefore, specifying the behavior of those systems has to be carried out carefully in order to avoid the side effects that might cause undesirable or even fateful behaviors. One of the primary concerns is the safety of the patient, which in turn leads to an extreme reliable, safe and robust robotic system. To our knowledge, no safety standards for robotic surgical systems are established yet. There is no common definition of the term safety in the context of robotic surgery and it is not easy to de ned. On the other hand, formal methods based on mathematical models are very convenient to design safety critical systems. They have been used extensively in different safety critical applications.

The main advantage of formal methods is that they provide a precise and obvious description of the behavior of the system under design. Additionally, they not only allow us to formally specify systems at different levels of abstraction, but also to verify the consistency of the specified systems before involving in the implementation phase. 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.

The contribution of this paper is to approach hybrid automata to surgical robots context by modeling a particular scenario between two surgical robots in a shared environment. The paper is doing so by modeling the mutual exclusion scenario between two robots sharing a critical working area. In particular, the pa- per focuses on the application of the mutual exclusion protocol at the OP: Sense Setup. The paper additionally shows some formal analysis of particular requirements on both simulation and model checking level.