Carnegie Mellon University researchers have come up with algorithms to help spot bugs in "cyber-physical systems" (CPS), those computerized mechanisms used to automate everything from aircraft collision avoidance to robotic surgery.
Their breakthrough, which involves analyzing the logic behind system design, has already been used to find a flaw in an aircraft collision avoidance maneuver that has since been corrected. In some ways, the technique is similar to Model Checking, a widely used method of spotting errors in complex hardware and software systems. CMU professor of computer science Edmund Clarke was behind Model Checking and is behind this latest research, this time along with Andre Platzer, an assistant professor of computer science at CMU.
"Engineers increasingly are relying on computers to improve the safety and precision of physical systems that must interact with the real world, whether they be adaptive cruise controls in automobiles or machines that monitor critically ill patients," Clarke said in a statement. "With systems becoming more and more complex, mere trial-and-error testing is unlikely to detect subtle problems in system design that can cause disastrous malfunctions. Our method is the first that can prove these complex cyber-physical systems operate as intended, or else generate counterexamples of how they can fail using computer simulation."
Detecting and fixing problems in CPS ahead of time could save transportation companies and others a lot of money, Platzer says, given that testing systems is currently so expensive.
The research is funded in part by the NSF and German Research Council.
Do you Tweet? Follow me on Twitter here