Hefty IT prof develops robot to check that robots are safe

Metal fink rats out air-traffic machine in trials

Top 5 reasons to deploy VMware with Tegile

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.

Beginner's guide to SSL certificates

More from The Register

next story
PORTAL TO ELSEWHERE scried in small galaxy far, far away
Supermassive black hole dominates titchy star formation
Boffins say they've got Lithium batteries the wrong way around
Surprises at the nano-scale mean our ideas about how they charge could be all wrong
Edge Research Lab to tackle chilly LOHAN's final test flight
Our US allies to probe potential Vulture 2 servo freeze
Europe prepares to INVADE comet: Rosetta landing site chosen
No word yet on whether backup site is labelled 'K'
Cracked it - Vulture 2 power podule fires servos for 4 HOURS
Pixhawk avionics juice issue sorted, onwards to Spaceport America
Archaeologists and robots on hunt for more Antikythera pieces
How much of the world's oldest computer can they find?
prev story


Secure remote control for conventional and virtual desktops
Balancing user privacy and privileged access, in accordance with compliance frameworks and legislation. Evaluating any potential remote control choice.
Intelligent flash storage arrays
Tegile Intelligent Storage Arrays with IntelliFlash helps IT boost storage utilization and effciency while delivering unmatched storage savings and performance.
WIN a very cool portable ZX Spectrum
Win a one-off portable Spectrum built by legendary hardware hacker Ben Heck
High Performance for All
While HPC is not new, it has traditionally been seen as a specialist area – is it now geared up to meet more mainstream requirements?
Beginner's guide to SSL certificates
De-mystify the technology involved and give you the information you need to make the best decision when considering your online security options.