Hefty IT prof develops robot to check that robots are safe

Metal fink rats out air-traffic machine in trials

Secure remote control for conventional and virtual desktops

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.

Next gen security for virtualised datacentres

More from The Register

next story
Gigantic toothless 'DRAGONS' dominated Earth's early skies
Gummy pterosaurs outlived toothy competitors
Vulture 2 takes a battering in 100km/h test run
Still in one piece, but we're going to need MORE POWER
TRIANGULAR orbits will help Rosetta to get up close with Comet 67P
Probe will be just 10km from Space Duck in October
Boffins ID freakish spine-smothered prehistoric critter: The CLAW gave it away
Bizarre-looking creature actually related to velvet worms
CRR-CRRRK, beep, beep: Mars space truck backs out of slippery sand trap
Curiosity finds new drilling target after course correction
'Leccy racer whacks petrols in Oz race
ELMOFO rakes in two wins in sanctioned race
What does a flashmob of 1,024 robots look like? Just like this
Sorry, Harvard, did you say kilobots or KILLER BOTS?
No sign of Ziggy Stardust and his band
Why your mum was WRONG about whiffy tattooed people
They're a future source of RENEWABLE ENERGY
prev story


5 things you didn’t know about cloud backup
IT departments are embracing cloud backup, but there’s a lot you need to know before choosing a service provider. Learn all the critical things you need to know.
Implementing global e-invoicing with guaranteed legal certainty
Explaining the role local tax compliance plays in successful supply chain management and e-business and how leading global brands are addressing this.
Build a business case: developing custom apps
Learn how to maximize the value of custom applications by accelerating and simplifying their development.
Rethinking backup and recovery in the modern data center
Combining intelligence, operational analytics, and automation to enable efficient, data-driven IT organizations using the HP ABR approach.
Next gen security for virtualised datacentres
Legacy security solutions are inefficient due to the architectural differences between physical and virtual environments.