Surgical robots could make some types of surgery safer and more effective, but proving that the software controlling these machines works as intended is problematic. So say researchers at Carnegie Mellon University, Pittsburgh, PA, and the Johns Hopkins University Applied Physics Laboratory, Baltimore, MD, who have demonstrated that methods for reliably detecting software bugs and ultimately verifying software safety can successfully be applied to these robots.

The researchers 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, they say, identified a safety flaw that could enable a scalpel or other surgical tool to malfunction, 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.

"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," says André Platzer, assistant professor of at Carnegie Mellon. Testing alone is inadequate because no test regimen can check all of the possible circumstances that the system might encounter.