Web proceedings papers


Luzie Schreiter , Ammar Mohammed , Joerg Raczkowsky and Heinz Woern


A Surgical robotic system is a computer assisted electro-mechanical device which helps the surgeon to perform interventions. It is a safety critical system as it has to take in consideration the safety of patients that can be violated due to technical problems. To respect the safety property some methods are needed to guarantee the correctness of the surgical system adherence to crucial safety requirements. For this reason, formal modeling and specification are helpful. This paper shows how to model and specify the coordination between safety critical surgical robots using hybrid automata. The approach allows formal system specification on different levels of abstraction on one hand, and the expression of real-time behavior of the system with continuous variables on the other hand. The semantics of hybrid automata allows us to analyze the robotics behavior using simulation or model checking