Bug spotting

Researchers at Carnegie Mellon University's School of Computer Science have developed a 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 (CPSs).
   
The approach, developed by Edmund M Clarke, the university's professor of computer science, and Andre Platzer, the assistant professor of computer science, has already detected a flaw in aircraft collision avoidance manoeuvres - which have since been corrected - that could have caused mid-air collisions.

It also has verified the soundness of the European Train Control System: a signalling, control and train protection system designed to replace the many incompatible safety systems currently used by European railways, especially on high-speed lines.
   
Clarke said: 'Engineers are increasingly 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.

'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 counter-examples of how they can fail using computer simulation,' he added.

As with model checking, a method pioneered by Clarke that is currently the most widely used technique for detecting and diagnosing errors in complex hardware and software design, the novel method analyses the logic underlying the system design.

A crucial difference, however, is that model checking can examine every possible state of a discrete finite-state system, such as a new circuit design for a computer chip; this is not possible for a CPS that must interact with the infinitely variable real world.

Even if the differential equations that govern these systems can be solved - and they often cannot - it is usually impossible to use the results to predict the behaviour of the system, Platzer said.

Instead, he and Clarke have developed algorithms that decompose the systems until they produce differential invariants: mathematical descriptions of the parts of the system that always remain the same. These differential invariants, in turn, can be used to prove that the CPS operates as intended.

The demand for such a method will only increase as these systems become more numerous and more crucial for everyday life, Platzer said.

'Bugs in complex cyber-physical systems - such as cars, aircraft, chips or medical devices - are expensive to fix and may endanger human life,' he explained. 'In transportation, the percentage of development cost spent on design and testing new control software is already well above 50 per cent and is steadily rising.'