When it comes to having robotic surgeons slicing around inside your brain, heart or other important body organ, surgeons and patients need to know that a software or hardware glitch isn't going to ruin their day.
That's why a new technique developed by researchers at Carnegie Mellon University and the Johns Hopkins University Applied Physics Laboratory that promises to reliably detect software bugs and verify the software safety surgical robots could be a significant development.
[RELATED: 11 cool robots you may not have heard of]
According to the researchers, surgical robots are an example of what they call a hybrid, or cyber-physical system - complex, computer-controlled devices that are becoming increasingly common. Other examples are aircraft collision avoidance systems, high-speed train controls and cars that avoid collisions, maintain their lanes or otherwise drive themselves.
"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," said André Platzer and assistant professor of computer science at Carnegie Mellon in a statement. Testing alone is inadequate because no test regimen can check all of the possible circumstances that the system might encounter, the researchers said.
What the researchers have developed is what they call a mathematical "tactics language for directing proof search, and implemented a new automated theorem prover called KeYmaeraD, an open source verification tool written in Scala.
From the research paper the group will present at the Hybrid Systems: "Computation and Control conference in Philadelphia this week: "We applied quantified differential-dynamic logic (QdL) to analyze a control algorithm designed to provide directional force feedback for a surgical robot. We identified problems with the algorithm, proved that it was in general unsafe, and described exactly what could go wrong. We then applied QdL to guide the development of a new algorithm that provides safe operation along with directional force feedback. Using KeYmaeraD, we created a machine-checked proof that guarantees the new algorithm is safe for all possible inputs." The method identified a safety flaw in the test robot that could enable 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.
The usual approach today for ensuring the safety of complex systems is careful design, thoughtful examination of the algorithms, and testing. These techniques analyze all the possible states of a system, much as a mathematician uses a proof to determine that a theorem is correct, the researchers said. But methods that work for computer circuitry or software, which may be complex but have a finite number of states, don't work for hybrid systems that must contend with the infinite variations of the physical world, the researchers stated.
"These techniques are going to change how people build robotic surgery systems," said Johns Hopkins' Yanni Kouskoulas, who led the research study with Platzer and others. The researchers say this formal verification technique also could change the way regulators evaluate new devices, providing more assurance of safety than is possible even with the most rigorous testing.
Check out these other hot stories: