This article is more than 1 year old

Hefty IT prof develops robot to check that robots are safe

Metal fink rats out air-traffic machine in trials

A Turing-awardwinner* boffin in the States says he has developed new software which can test the safety of computer-controlled railways, air-traffic systems, hospital intensive-care monitors, enormous 600-tonne godzilla lorries and such like - all the many kinds of smart machinery which can kill people.

Automated "roundabout" air-traffic procedures don't always work

Computer says "prang"

Professor Edmund Clarke of Carnegie Mellon Uni, joint winner of the 2007 Turing Award, describes automated things which can kill you if they go wrong as "cyber-physical" systems. He and his assisant prof Andre Platzer say that cyber-physical systems are proliferating madly, and there's a lot more to come. Ideas such as smart energy grids, automated satnav-driven air traffic, self-driving or partially self-driving cars - and, of course, killer war robots - will be so complicated and potentially deadly that normal tests will never uncover all the ways they could go wrong.

"Bugs in complex cyber-physical systems like cars, aircraft, chips or medical devices are expensive to fix and may endanger human life," explains Platzer. "In transportation, the percentage of development cost spent on design and testing new control software is already well above 50 percent and is steadily rising."

The answer, according to Clarke and Platzer, is to skip out trial-and-error testing and instead use their new cyber-physical systems safety verifier. They say their new tech has already sniffed out a potentially fatal flaw in a system of "roundabouts" used in air-traffic control:

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.

"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," says Clarke.

"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."

In reassuring news for European rail passengers, it seems that the new kit has had a look at the continent's rail-signalling controls and given them a clean bill of health, finding no ways in which absentminded computers might accidentally ram trains into each other.

The new methods represent a step forward on "Model Checking", the technique which won Clarke his Turing. Model Checking works within finite-state systems like hardware and software design, and is widely used in such fields. But in a cyber-physical system where the real world injects infinite variability, the black-white-and-only-so-many-shades-of-grey Model Checking approach can't be used.

Hence the new toolset, which (obviously, duh) uses "algorithms that decompose the systems until they produce differential invariants — mathematical descriptions of parts of the system that always remain the same [and] can be used to prove the global logic".

No? Actually we didn't understand it either.

"Finding the [bugs] is actually the easy part," says Platzer. "Proving that they're fixed is hard."

It was clearly up to Carnegie Mellon to come up with something of this sort, anyway: as the institution which gave the world the 600-tonne robotic godzilla-lorry, it was incumbent on them to make such things safe.

One question does spring to mind, though. Presumably the robotic safety checker should itself be checked for infallibility, either using Model Checking or a version of itself. There's more on the new test-ware from Carnegie Mellon here. ®

*The Turing award is often described as the Nobel Prize in computing.

More about

TIP US OFF

Send us news


Other stories you might like