OK We use cookies to enhance your visit to our site and to bring you advertisements that might interest you. Read our Privacy and Cookies policies to find out more.
OK We use cookies to enhance your visit to our site and to bring you advertisements that might interest you. Read our Privacy and Cookies policies to find out more.

News Americas

Methods for reliably detecting software bugs and ultimately verifying software safety can be applied successfully to surgical robots. (Photo: Jovan Nikolic/Shutterstock)
Apr 19, 2013 | News Americas

New technique finds software bugs in surgical robots

by Surgical Tribune

PITTSBURGH, Pa., USA: Surgical robots could make some types of surgery safer and more effective; however, proving that the software controlling these machines works as intended is problematic. Researchers have now demonstrated that methods for reliably detecting software bugs and ultimately verifying software safety can be applied successfully to this breed of robot.

Researchers at Carnegie Mellon University and the Johns Hopkins University Applied Physics Laboratory used theorem-proving techniques to analyze a control algorithm for a research robot that would help a surgeon perform surgery at the base of the skull. Their method identified a safety flaw that could allow a scalpel or other surgical tool to go dangerously astray in this area, where the eye orbits, ear canals, and major arteries and nerves are closely spaced and vulnerable to injury. It also guided development of a new algorithm and verified that the new controller was safe and reliable.

"These techniques are going to change how people build robotic surgery systems," predicted the laboratory's Yanni Kouskoulas, who led the study with André Platzer, assistant professor of computer science at Carnegie Mellon. Platzer and Kouskoulas say this formal verification technique could also change the way regulators evaluate new devices, providing greater safety assurance than is possible even with the most rigorous testing.

Surgical robots are an example of a hybrid or cyber-physical system — complex, computer-controlled devices that are becoming increasingly common. "Because the consequences of these systems malfunctioning are so great, finding a way to prove they are free of design errors has been one of the most important and pressing challenges in computer science," Platzer said. Testing alone is inadequate because no test regimen can check all of the possible circumstances that the system might encounter.

A growing number of techniques have been developed to aid in formally verifying that computer hardware and software are free from design defects. However, methods that work for computer circuitry or software, which may be complex but have a finite number of states, do not work for hybrid systems that must contend with the infinite variations of the physical world.

Platzer, however, has developed an approach based on differential dynamic logic and an associated tool called KeYmaeraD that can be used to model a hybrid system and its properties and then pick it apart. This approach, which Platzer has already used successfully to identify errors in aircraft collision avoidance systems and to verify the design of distributed car control systems, can verify that a design is safe or else help generate counterexamples of how the system could fail.

Platzer and his colleagues applied this approach to evaluate the control algorithm for the skull-base surgery robot. This robot aids in intricate surgery in small recesses of the brain by minimizing tiny movements as a surgeon manipulates a tool and by restricting the tool to movement within the surgical site. As the tool approaches the surgical boundary, beyond which healthy and vital tissues can be harmed, it exerts force feedback to warn the surgeon. If the tool reaches the boundary, the robot is supposed to prevent it from going farther. This functionality is helpful for the surgeon because the robot knows the delicate boundaries that the surgeon cannot necessarily see during the surgery.

Kouskoulas said the robot and the control algorithm were tested extensively, including on cadavers. "While it worked in the configurations in which it was tested, the fear was always that something unexpected could go wrong," he noted.

By using the formal verification method, the researchers demonstrated that something unexpected could indeed occur in corners of the surgical site. They found that in some geometrical configurations, the safety feedback for one boundary would interfere with that of the adjoining boundary, cancelling each other out and allowing the tool to pass beyond the limits set by the surgeon.

KeYmaeraD generated examples of how this could occur. "It leads you to the problem," Kouskoulas explained. "You then have to be creative to find the solution." With that guidance, researchers were able to devise a new algorithm and use their method to prove it was safe.

"Medical robotics is an interesting problem area for hybrid systems," Platzer said. Existing certification procedures, which rely on trial-and-error testing, are not appropriate for evaluating these software-intensive devices, he said. This study demonstrates that formal verification methods can be applied successfully to medical robotics and that further development is warranted, he added.

The study was supported by the National Science Foundation.

RELATED ARTICLES
Print  |  Send to a friend