Application of contract-based verification techniques for hybrid automata to surgical robotic systems

Surgical robotic systems have to deliver a high quality of safety, since they deal with human lives. Their safety specifications must ensure the absence of risks for the patient and the operating room staff. To respect the modular nature of a surgical system, we propose a contract based verification approach for safety. We introduce a case study based on a typical surgical robotic operation scenario and model its components by using hybrid automata. We exploit the theory of parallel composition of contracts to verify properties on each component and prove that the property of the overall system can be obtained by composition.