WASHINGTON - Scientists have developed a new method for systematically identifying bugs in aircraft collision avoidance systems, high-speed train controls and other complex, computer-controlled devices, collectively known as cyber-physical systems (CPS).
The approach, developed by Edmund M. Clarke and Andre Platzer from Carnegie Mellon University’s School of Computer Science, has already detected a flaw in aircraft collision avoidance maneuvers that could have caused mid-air collisions.
It also has verified the soundness of the European Train Control System.
Ultimately, the method could be used on other cyber-physical systems, such as robotic surgery devices and nano-level manufacturing equipment.
“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,” Clarke said.
“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,” he added.
In the case of aircraft collision avoidance systems, for instance, Platzer and Clarke used their method to analyze so-called roundabout maneuvers.
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.
The new method analyzes the logic underlying the system design, much as a mathematician uses a proof to determine that a theorem is correct.
Platzer and Clarke have developed algorithms that decompose the systems until they produce differential invariants - mathematical descriptions of parts of the system that always remain the same.
These differential invariants, in turn, can be used to prove the global logic of the CPS.
“When the system design is sound, as we found in the case of the European control system for train traffic or the repaired flight controller, our method can provide conclusive proof,” Platzer said.
Likewise, when flaws exist, the method reliably generates counterexamples.
The demand for methods that can prove a CPS or hybrid system operates as intended will only increase as these systems become more numerous and more crucial for everyday life. (ANI)
Related News
Extremely fast computers come a step closer to realitySeptember 28th, 2009 WASHINGTON - Physicists at UC (University of California) San Diego have successfully created speedy integrated circuits with particles called "excitons" that operate at commercially cold temperatures, bringing the possibility of a new type of extremely fast computer based on excitons closer to reality. Their discovery follows the team's demonstration last summer of an integrated circuit-an assembly of transistors that is the building block for all electronic devices-capable of working at 1.5 degrees Kelvin above absolute zero.
Institute of Medicine will review FDA's system for clearing low-risk medical devicesSeptember 23rd, 2009 FDA medical device approvals get external reviewWASHINGTON — The Food and Drug Administration is asking the government's top medical advisers to review its system for approving certain types of medical devices, which has been criticized by safety advocates and government watchdogs. The nonprofit Institute of Medicine will conduct a two-year review of FDA's so-called 510k review procedure, which allows device companies to quickly launch products similar to those already on the market.
New computing tool may help scientists create tastier and longer lasting tomatoesSeptember 23rd, 2009 WASHINGTON - Scientists have developed a new computing tool that could help scientists predict how plants will react to different environmental conditions in order to create better crops, such as tastier and longer lasting tomatoes. The tool will form part of a new 1.7 million pounds Syngenta University Centre at Imperial College London, which will see researchers from Imperial and Syngenta working together to improve agricultural products.
New graphite-based nano-material may herald next generation of electronic devicesSeptember 3rd, 2009 WASHINGTON - An international team of researchers has designed a new graphite-based, magnetic nano-material that acts as a semiconductor and could help material scientists create the next generation of electronic devices like microchips. The nano-material was designed by a team of researchers from Virginia Commonwealth University (VCU); Peking University in Beijing, China; the Chinese Academy of Science in Shanghai, China; and Tohoku University in Sedai, Japan.
Scientists propose new way to reproduce a black hole in the labAugust 22nd, 2009 WASHINGTON - In a new research, a team of scientists at Dartmouth university has proposed a new way of creating a reproduction black hole in the laboratory on a much-tinier scale than their celestial counterparts. The new method to create a tiny quantum sized black hole would allow researchers to better understand what physicist Stephen Hawking proposed more than 35 years ago: black holes are not totally void of activity; they emit photons, which is now known as Hawking radiation.
Scientists develop faster, cheaper DNA test for crimesJuly 9th, 2009 WASHINGTON - Scientists in Japan have developed a faster, cheaper and better DNA test for criminal investigations, diagnostics and other applications, according to the latest research. They reported a superior version of the fabled polymerase chain reaction (PCR) a DNA test, that works by amplifying "previously undetectable traces of DNA almost like photo-copiers produce copies of documents," noted Naohiro Noda and colleagues.
Soon, wheelchairs controlled by tonguesJuly 1st, 2009 WASHINGTON - Scientists have developed a novel headset that makes it possible for a person suffering from spinal cord injury to precisely control a wheelchair or computer using the tongue. The "tongue drive", being trialled at Georgia Tech University, Atlanta, could also give astronauts a third hand in difficult situations like spacewalks.
New technique to detect metabolites from a single drop of bloodJune 19th, 2009 WASHINGTON - A single drop of blood could soon be able to identify various blood related metabolites-such as sugars, fatty acids, amino acids and other organic substances-from plant or animal tissue samples. Scientists at the Max Planck Institute for Chemical Ecology in Jena and their colleagues from the Czech Academy of Sciences in Prague have developed a new method to quickly and reliably detect metabolites from only a drop of blood.
Scientists develop new tool to visualize past and future lunar eclipsesJune 9th, 2009 WASHINGTON - Researchers at Rensselaer Polytechnic Institute, US, have developed a new method for using computer graphics to simulate and render an accurate visualization of a lunar eclipse, whether in the past or in the future. The model uses celestial geometry of the sun, Earth, and moon, along with data for the Earth's atmosphere and the moon's peculiar optical properties to create picture-perfect images of lunar eclipses.
Nano-raspberries may fight foggy windows, eyeglassesMay 25th, 2009 WASHINGTON - Fogged-up car windshield is a safety hazard and a nuisance that affect millions of people. Existing technology, including sprays that must be reapplied to stay effective, has many drawbacks.
Scientists power artificial cells with non-stop mobilityMay 5th, 2009 WASHINGTON - Scientists are developing artificial cells with the ability to tap an energy source and use it for sustained mobility. A Japanese study described the first 'self-propelled' oil droplets (used as a model for research on artificial cells) that can run on a chemical 'fuel'.
Genes that protect against aging identifiedApril 21st, 2009 WASHINGTON - University of Liverpool researchers have developed a novel method to help scientists identify genes that can help protect the body during the ageing process. The team developed a method of analysing genes in multiple ageing tissue types in both animals and humans.
Now, 'racetrack' memory for PCs to beat 'back-up' bluesApril 4th, 2009 WASHINGTON - No need to panic if your hard disk is about to crash and you have not yet copied your favourite pictures and notes on a CD, for a new kind of computer memory may soon make 'back-up' a thing of the past. Racetrack memory, developed by Physicists at the University of Leeds and scientists at IBM Research's Zurich lab, may become the standard method of storing information in home computers.
Now, a computer that can work like a scientist to derive natural lawsApril 3rd, 2009 WASHINGTON - Researchers at Cornell University, US, using a computer, have developed an algorithm which can derive natural laws from observed data, just like scientists. What the researchers have done is to teach a computer to find regularities in the natural world that become established laws - yet without any prior scientific knowledge on the part of the computer.
Engineers revolutionise nano-device fabricationFebruary 11th, 2009 WASHINGTON - Engineers have created a process that may revolutionise the manufacture of nano-devices from computer memory to biomedical sensors by exploiting a novel type of metal. The material can be moulded like plastics to create features at the nano-scale and yet is more durable and stronger than silicon or steel.
Loading ...