Provable Safety in Medical Robotics

Medical robotics promises important advances in medical care, especially when medical robots help and complement expert medical doctors and practitioners. Due to their direct impact on the health of the patient, medical robots and their control algorithms need to meet stringent safety requirements that are challenging for classical FDA / EMA / TÜV approval processes for medical devices. Mathematical proofs of safety of controllers for physical models of the medical robot provide a possible way out. The potential of this approach has been demonstrated for a surgical robot for skull-base surgery, in which two errors were identified and fixed thanks to safety proofs with a theorem prover in the PI's KeYmaera family. Depending on the circumstances, one of those errors in the safety control can cause safety hazards that it was designed to prevent. These mistakes had not been found previously despite state-of-the art software engineering, testing and validation, but were so subtle that they needed proofs.