Feeds

Hefty IT prof develops robot to check that robots are safe

Metal fink rats out air-traffic machine in trials

Intelligent flash storage arrays

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.

Intelligent flash storage arrays

More from The Register

next story
Boffins who stare at goats: I do believe they’re SHRINKING
Alpine chamois being squashed by global warming
Comet Siding Spring revealed as flying molehill
Hiding from this space pimple isn't going to do humanity's reputation any good
Experts brand LOHAN's squeaky-clean box
Phytosanitary treatment renders Vulture 2 crate fit for export
LONG ARM of the SAUR: Brachially gifted dino bone conundrum solved
Deinocheirus mirificus was a bit of a knuckle dragger
MARS NEEDS WOMEN, claims NASA pseudo 'naut: They eat less
'Some might find this idea offensive' boffin admits
No sail: NASA spikes Sunjammer
'Solar sail' demonstrator project binned
Carry On Cosmonaut: Willful Child is a poor taste Star Trek parody
Cringeworthy, crude and crass jokes abound in Steven Erikson’s sci-fi debut
prev story

Whitepapers

Cloud and hybrid-cloud data protection for VMware
Learn how quick and easy it is to configure backups and perform restores for VMware environments.
A strategic approach to identity relationship management
ForgeRock commissioned Forrester to evaluate companies’ IAM practices and requirements when it comes to customer-facing scenarios versus employee-facing ones.
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?
Three 1TB solid state scorchers up for grabs
Big SSDs can be expensive but think big and think free because you could be the lucky winner of one of three 1TB Samsung SSD 840 EVO drives that we’re giving away worth over £300 apiece.
Security for virtualized datacentres
Legacy security solutions are inefficient due to the architectural differences between physical and virtual environments.