Scientists develop method for verifying safety of computer-controlled devicesApril 21st, 2009 - 4:50 pm ICT by ANI
Washington, April 21 (ANI): 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)
- India creating architecture to ensure cyber security: NSA - May 16, 2012
- Carnegie Mellon's soccer-playing robots use physics to score a goal - Jun 04, 2010
- Cold streams of gas pushed huge growth in black holes - Dec 14, 2011
- Online searchers can help strangers make sense of data - May 08, 2012
- Self-driven cars come closer to reality - Jun 01, 2010
- 'Intelligent co-pilot' makes driving safer - Jul 15, 2012
- 'Citizen scientists' could tackle environmental disasters - Sep 26, 2010
- Symantec to unveil strategies against cyber attacks (Lead) - Dec 01, 2010
- 'Touche' gives human touch to doorknobs, smartphones - May 06, 2012
- Newly developed smart camera can track individuals at any angle - Apr 15, 2011
- Cyber arms race could change the world around us (Comment) - Jun 27, 2012
- Unprecedented cyber attack on Canada linked to China - Feb 17, 2011
- 8,000 cyber attacks warded off during CWG: NSA - May 16, 2012
- Indian origin scientist develops new projection technology - Jul 07, 2010
- For teens online tagged photos more precious than actual ones - May 10, 2011
Tags: carnegie mellon researchers, carnegie mellon university, collision avoidance systems, collision course, computer simulation, counterexample, european train, high speed train, maneuver, maneuvers, manufacturing equipment, mid air collisions, platzer, robotic surgery, soundness, subtle problems, traffic circle, train control system, train controls, using computer