Scientists develop method for verifying safety of computer-controlled devices

Washington, April 21 (ANI): Scientists have developed a new method for systematically identifying bugs in aircraft collision avoidance systems, high-speed train controls and other complex, computer-controlled devices, collectively known as cyber-physical systems (CPS).

The approach, developed by Edmund M. Clarke and Andre Platzer from Carnegie Mellon University's School of Computer Science, has already detected a flaw in aircraft collision avoidance maneuvers that could have caused mid-air collisions.

It also has verified the soundness of the European Train Control System.

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, or else generate counterexamples of how they can fail using computer simulation," he added.

In the case of aircraft collision avoidance systems, for instance, Platzer and Clarke used their method to analyze so-called roundabout maneuvers.

When two aircraft are on rapidly converging paths, one technique for avoiding collisions is for the system to order each pilot to turn right and then circle to the left until the aircraft can safely turn right again to resume their original paths.

It's as if the aircraft are following a large traffic circle, or rotary, in the sky. But, analysis by the Carnegie Mellon researchers identified a counterexample.

When aircraft approach each other at certain angles, the roundabout maneuver actually creates a new collision course that, in the few seconds remaining before their paths cross, the pilots might not have time to recognize.

The new method analyzes the logic underlying the system design, much as a mathematician uses a proof to determine that a theorem is correct.

Platzer and Clarke have developed algorithms that decompose the systems until they produce differential invariants - mathematical descriptions of parts of the system that always remain the same.

These differential invariants, in turn, can be used to prove the global logic of the CPS.

"When the system design is sound, as we found in the case of the European control system for train traffic or the repaired flight controller, our method can provide conclusive proof," Platzer said.

Likewise, when flaws exist, the method reliably generates counterexamples.

The demand for methods that can prove a CPS or hybrid system operates as intended will only increase as these systems become more numerous and more crucial for everyday life. (ANI)