Flaw-finding analysis could boost safety margins
A method for systematically identifying bugs in complex, computer-controlled devices – or cyber-physical systems (CPS) – such as aircraft collision avoidance systems, and high-speed train controls, has been unveiled by researchers at Pittsburgh’s Carnegie Mellon University.
With the working designation of ‘differential invariants as fixedpoints’ (DIF), its developers, Professor of Computer Science Edmund Clarke, and assistant professor of computer science Andre Platzer, say the approach has already has found a flaw – now corrected – in aircraft collision avoidance maneuvers that could have caused a mid-air collision.
DIF analyses the logic underlying the system design, much as a mathematician uses a proof to determine that a theorem is correct; it has similarities to Model Checking, a technique pioneered by Professor Clarke that is used for detecting and diagnosing errors in complex hardware and software design. However, where a CPS must interact with the infinitely variable real world, DIF employs 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 a CPS operation.
“Engineers rely on computers to improve the safety and precision of physical systems that interact with the real world, such as adaptive cruise controls in cars, or machines that monitor critically-ill patients,” explains Professor Clarke, “but trial-and-error testing is unlikely to detect subtler problems in system design that can cause malfunctions. Even when system design is sound, DIF can prove these complex CPSs do operate as intended, or it can generate counter-examples of how they can fail, using computer simulation.”
DIF should be most helpful in the design or redesign process of CPSs, Andre Platzer told E&T: “Most crucial questions arise while designing system controllers, like, for instance, what controller architecture to use or how to choose control parameters of the system. Like with desktop software, good or bad early design decisions have most impact on embedded software: that’s when verification is most helpful to analyse if the model will work as intended, or to discover what can go wrong.”
The method could be ultimately be used on other cyber-physical systems, such as robotic surgery devices, and nano-level manufacturing equipment, Clarke and Platzer add.
More IT section news.