Researchers at Carnegie Mellon University's School of Computer Science have developed a new method for systematically identifying bugs in aircraft collision avoidance systems, high-speed train controls and other complex, computer-controlled devices. The approach, developed by University Professor of Computer Science Edmund M. Clarke and Andre Platzer, assistant professor of computer science, already has detected a flaw in aircraft collision avoidance maneuvers — since corrected — that could have caused mid-air collisions. Ultimately, the method could be used on other cyber-physical systems, such as robotic surgery devices and nano-level manufacturing equipment.
"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," Clarke said. "Our method is the first that can prove these complex cyber-physical systems operate as intended."
View Full Article