Forum for Science, Industry and Business

Sponsored by:     3M 
Search our Site:

 

Scientists develop method for verifying safety of computer-controlled devices

22.04.2009
Researchers at Carnegie Mellon University's School of Computer Science 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 University Professor of Computer Science Edmund M. Clarke and Andre Platzer, assistant professor of computer science, already has detected a flaw in aircraft collision avoidance maneuvers —since corrected — 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.

"Engineers increasingly are relying on computers to improve the safety and precision of physical systems that must interact with the real world, whether they be adaptive cruise controls in automobiles or machines that monitor critically ill patients," Clarke said. "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. 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 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.

Like Model Checking, a method pioneered by Clarke that today is the most widely used technique for detecting and diagnosing errors in complex hardware and software design, the new method analyzes the logic underlying the system design, much as a mathematician uses a proof to determine that a theorem is correct. Clarke shared the 2007 A.M. Turing Award, generally considered the computer science equivalent of the Nobel Prize, for his role in developing Model Checking.

A crucial difference, however, is that Model Checking can examine every possible state of a discrete finite-state system, such as a new circuit design for a computer chip; that's not possible for a CPS that must interact with the infinitely variable real world. Even if the differential equations that govern these systems can be solved — and they often can't — it usually is impossible to use the results to predict the behavior of the system, Platzer said. Instead, he 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. "Finding the counterexamples is actually the easy part," he added. "Proving that they are fixed is hard."

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, Platzer said. "Bugs in complex cyber-physical systems like cars, aircraft, chips or medical devices are expensive to fix and may endanger human life," he explained. "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 National Science Foundation (NSF) has identified the design and verification of CPS as a key area of research. The increasing use of robotic devices, the growth of sensor networks, the proposed creation of a "smart grid" for delivering electrical power, a greater reliance on automated war fighting and growing use of efficient, "zero-net-energy" buildings are all examples of a growing reliance on computer control systems that are tightly coupled to physical systems. This work was sponsored, in part, by the NSF and the German Research Council.

About Carnegie Mellon: Carnegie Mellon is a private research university with a distinctive mix of programs in engineering, computer science, robotics, business, public policy, science and social science, fine arts and the humanities. More than 11,000 undergraduate and graduate students receive an education characterized by its focus on creating and implementing solutions for real problems, interdisciplinary collaboration, and innovation. A small student-to-faculty ratio provides an opportunity for close interaction between students and professors. While technology is pervasive on its 145-acre Pittsburgh campus, Carnegie Mellon is also distinctive among leading research universities for the world-renowned programs in its College of Fine Arts. A global university, Carnegie Mellon has campuses California's Silicon Valley and Qatar, and programs in Asia, Australia and Europe.

Byron Spice | EurekAlert!
Further information:
http://www.cmu.edu

More articles from Information Technology:

nachricht Construction of practical quantum computers radically simplified
05.12.2016 | University of Sussex

nachricht UT professor develops algorithm to improve online mapping of disaster areas
29.11.2016 | University of Tennessee at Knoxville

All articles from Information Technology >>>

The most recent press releases about innovation >>>

Die letzten 5 Focus-News des innovations-reports im Überblick:

Im Focus: Significantly more productivity in USP lasers

In recent years, lasers with ultrashort pulses (USP) down to the femtosecond range have become established on an industrial scale. They could advance some applications with the much-lauded “cold ablation” – if that meant they would then achieve more throughput. A new generation of process engineering that will address this issue in particular will be discussed at the “4th UKP Workshop – Ultrafast Laser Technology” in April 2017.

Even back in the 1990s, scientists were comparing materials processing with nanosecond, picosecond and femtosesecond pulses. The result was surprising:...

Im Focus: Shape matters when light meets atom

Mapping the interaction of a single atom with a single photon may inform design of quantum devices

Have you ever wondered how you see the world? Vision is about photons of light, which are packets of energy, interacting with the atoms or molecules in what...

Im Focus: Novel silicon etching technique crafts 3-D gradient refractive index micro-optics

A multi-institutional research collaboration has created a novel approach for fabricating three-dimensional micro-optics through the shape-defined formation of porous silicon (PSi), with broad impacts in integrated optoelectronics, imaging, and photovoltaics.

Working with colleagues at Stanford and The Dow Chemical Company, researchers at the University of Illinois at Urbana-Champaign fabricated 3-D birefringent...

Im Focus: Quantum Particles Form Droplets

In experiments with magnetic atoms conducted at extremely low temperatures, scientists have demonstrated a unique phase of matter: The atoms form a new type of quantum liquid or quantum droplet state. These so called quantum droplets may preserve their form in absence of external confinement because of quantum effects. The joint team of experimental physicists from Innsbruck and theoretical physicists from Hannover report on their findings in the journal Physical Review X.

“Our Quantum droplets are in the gas phase but they still drop like a rock,” explains experimental physicist Francesca Ferlaino when talking about the...

Im Focus: MADMAX: Max Planck Institute for Physics takes up axion research

The Max Planck Institute for Physics (MPP) is opening up a new research field. A workshop from November 21 - 22, 2016 will mark the start of activities for an innovative axion experiment. Axions are still only purely hypothetical particles. Their detection could solve two fundamental problems in particle physics: What dark matter consists of and why it has not yet been possible to directly observe a CP violation for the strong interaction.

The “MADMAX” project is the MPP’s commitment to axion research. Axions are so far only a theoretical prediction and are difficult to detect: on the one hand,...

All Focus news of the innovation-report >>>

Anzeige

Anzeige

Event News

ICTM Conference 2017: Production technology for turbomachine manufacturing of the future

16.11.2016 | Event News

Innovation Day Laser Technology – Laser Additive Manufacturing

01.11.2016 | Event News

#IC2S2: When Social Science meets Computer Science - GESIS will host the IC2S2 conference 2017

14.10.2016 | Event News

 
Latest News

Closing the carbon loop

08.12.2016 | Life Sciences

Applicability of dynamic facilitation theory to binary hard disk systems

08.12.2016 | Physics and Astronomy

Scientists track chemical and structural evolution of catalytic nanoparticles in 3-D

08.12.2016 | Materials Sciences

VideoLinks
B2B-VideoLinks
More VideoLinks >>>