Monitoring da Vinci, Safety Managed by a Robot. A study into Runtime Verification and Monitoring Systems for Robot-Assisted Surgery.

Abstract

Research into robot-assisted surgery (RAS) continues to grow each year. However, RAS is complex and requires extensive surgical training to acquire a sufficient proficiency level to master the skill of accurately controlling the surgical robot that is used for RAS. The most widely used robotic surgical system is named the da Vinci surgical system. Implementing a system that monitors the actions of the surgeon into the digital environment of the da Vinci surgical system could check the correctness of these actions (verification) at the actual time the action is performed (runtime). The objective of this research is to provide the grounds for a Runtime Verification (RV) system to be used during Robot-Assisted Surgery to improve the patient safety by preventing inadvertent damages and complications during surgery. To test the workings and the significance of a RV monitoring system in RAS, we present three examples of surgical behaviour that could potentially lead to damages and complications based on the use case of the robot-assisted minimally invasive esophagec- tomy (RAMIE) procedure. We have simulated these examples in a digital simulation environment and integrated a RV system to monitor the movements and motions of a 3D model of the da Vinci surgical system in a model of the thorax of a patient. We identi- fied suitable formal languages and designed properties to detect undesired behaviour of the da Vinci robot. The monitor checks the behaviour against formal safety properties specified in signal temporal logic and issues a warning in the event a property is likely to be violated, with the idea to alert the surgeon of undesired behavioural activity before complications would arise during surgery. Our constructed proof-of-concept RV system successfully simulated the monitoring of damage done to the aorta in a real-life surgical video as well as synthetic examples of hasty and hesitant movements of the robot arms. Experimental evaluation of these simulations demonstrate that detection of this undesired behaviour in runtime through the integrated RV system would have given a warning to the surgeon to not come in closer proximity to the aorta and would likely have mitigated and prevented the damage that was caused to the aorta. The ability to monitor movements of the components of the da Vinci surgical system applies to other parameters, like for example the speed of these components, aiding in preventing other undesired scenarios that could happen during RAS procedures and therefore increasing the safety of the patient in general. Finally, we generalize our results and outline future possibilities for integrating run- time verification into the field of robot-assisted surgery.