Researcher helps improve algorithm for robotic surgeons
Even the most experienced and skilled surgeons find surgery to be an arduous and stressful task. The emergence of medical robots that assist surgeons has allowed many surgeries to become significantly safer and more effective. However, before these robots can be utilized in the field, engineers must be certain that the robot will react accordingly in every possible situation that may arise during a surgery. Computer scientists at Carnegie Mellon teamed up with physicists and engineers from Johns Hopkins University to develop a universal method of using logical reasoning to identify bugs in medical robots and make sure they perform their required functions successfully.
Researcher Yanni Kouskoulas and his team at the Applied Physics Laboratory at Johns Hopkins University initially designed a medical robot that would aid a surgeon in preforming a surgical procedure at the base of the skull. During the surgery, it is very important for a surgeon to ensure that he or she doesn’t accidentally damage nearby parts of the body. This can pose a larger problem when the surgeon fails to have a full view of the surgical space.
To ensure the safety of the patient, the doctor can use imaging techniques such as Magnetic Resonance Imaging (MRI) or Computed Tomomgraphy (CT) scans to establish the boundaries of the surgical space. The robot recognizes these boundaries and aids surgeons by applying resistance to their movement as they get closer to the edges. It also prevents doctors from leaving the surgical space altogether.
While testing the robot on cadavers, Kouskoulas and his team realized that the robot exhibited undefined behavior in some rare cases. Confused about the source of their problem, Kouskoulas and his team reached out to André Platzer, a professor of computer science at Carnegie Mellon, to help them evaluate their system and determine where they were going wrong.
Platzer has been actively working on developing tools to verify the correctness of cyber-physical systems, which combine computation and physical movements. Normal proofs in computer science are not sufficient because they do not account for the infinite possible states of a physical application. In the past few years, his tools have successfully verified and increased the safety of railway control systems and air traffic control systems.
The verification tool, known as KeYmaeraD, is a mathematical proof that aims to systematically study a system and prove that a condition always holds true. The proof examines the various states of the robot system and ensures that the tools always remain within established boundaries. In many different cases, the proof works automatically. However, when the proof fails, the tool presents a counterexample by highlighting the specific situation where the system fails.
Soon after Platzer and Kouskoulas met and began to establish their proof, they highlighted a significant problem in the system: The robot checked a movement in relation to each of the edges of the surgical space one by one and initiated resistance if the movement was too close to the boundary. However, in the process of moving to the next boundary, the robot would undo the resistance that was just established in order to make a new one.
After identifying a problem, changing an established design can be a challenging process: Kouskoulas and his team faced the challenge, making many modifications to their system based on the results of Platzer’s verification tool. They continued testing until every single state could be proven. The newly designed system did not exhibit unexpected behavior during testing on cadavers.
Platzer explained that using a verification tool can enhance the testing process because it immediately identifies where a system might fail. In addition, complications during surgery can be unexpected and it is impossible to test the infinite states of the system on a cadaver. With such a tool, the robot’s engineers can be sure that the robot will always exhibit the correct outcome during a surgery, ensuring the safety of the patient.
The principles used to test and prove the skull-based surgery system can be applied to a variety of surgical robot models all based on establishing boundaries and ensuring that a doctor remains within the surgical space. Platzer hopes that formal verification tools will help engineers design safer medical robots by identifying the various situations where the system might fail before being used in surgery.