Feeds

Hefty IT prof develops robot to check that robots are safe

Metal fink rats out air-traffic machine in trials

5 things you didn’t know about cloud backup

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.

Secure remote control for conventional and virtual desktops

More from The Register

next story
Boffins attempt to prove the UNIVERSE IS JUST A HOLOGRAM
Is this the real life? Is this just fantasy?
Our LOHAN spaceplane ballocket Kickstarter climbs through £8000
Through 25 per cent but more is needed: Get your UNIQUE rewards!
Software bug caught Galileo sats in landslide, no escape from reality
Life had just begun, code error means Russia's gone and thrown it all away
LOHAN tunes into ultra long range radio
And verily, Vultures shall speak status unto distant receivers
NASA to reformat Opportunity rover's memory from 125 million miles away
Interplanetary admins will back up data and get to work
SpaceX prototype rocket EXPLODES over Texas. 'Tricky' biz, says Elon Musk
No injuries or near injuries. Flight stayed in designated area
Galileo, Galileo! Galileo, Galileo! Galileo fit to go. Magnifico
I'm just a poor boy, nobody loves me. But at least I can find my way with ESA GPS by 2017
prev story

Whitepapers

Gartner critical capabilities for enterprise endpoint backup
Learn why inSync received the highest overall rating from Druva and is the top choice for the mobile workforce.
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.
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.
Consolidation: The Foundation for IT Business Transformation
In this whitepaper learn how effective consolidation of IT and business resources can enable multiple, meaningful business benefits.
Next gen security for virtualised datacentres
Legacy security solutions are inefficient due to the architectural differences between physical and virtual environments.