Two commercial jetliners flying at high altitude above a major American city—both carrying hundreds of passengers—are heading toward each other. There is little time to spare before they will collide. Somehow, this impending crash goes undetected by the flight directors at the nearby Air Route Traffic Control Center, whose job it is to route plane traffic through the city's airspace. And somehow, neither pilot notices the pending head-on collision.
With the planes hurtling toward each other at speeds upward of 500 miles per hour, the on-board traffic alert system sounds an alarm. The pilots must act, and act immediately. In these last-resort situations, pilots are taught to rely on a standard collision-avoidance protocol designed to help prevent tragedies like the 2002 mid-flight crash in Überlingen, Germany, that killed all 71 passengers aboard both aircraft.
There is one roundabout procedure in particular, not yet implemented, which calls upon planes with intersecting flight paths to bank right and then curve back smoothly to the left until it is safe to resume their original flight paths, almost as if the pilots were following a rotary in the sky in opposite directions. The proposed plan was first introduced a decade ago, and three papers have been published demonstrating that the concept is fail-safe. The Federal Aviation Administration is considering recommending this course of action in its Next Generation Air Transportation System, an ongoing overhaul of the nation's airspace system that aims to make plane travel safer and more efficient.
That's why André Platzer was baffled by the results on his screen.
It was the summer of 2006, and the computer science PhD student was visiting Carnegie Mellon from the University of Oldenburg in Germany. There, he developed a new computer tool that can verify how a system could react given any set of circumstances. Because the roundabout tactic had been documented as foolproof, he decided to use it as a simple test to confirm that his computer program was glitch-free by not detecting any problems in the collision-avoidance sequence.
Yet, time and again, his program told him that if two aircraft were heading toward each other at 45-degree angles, the bank-right action meant to save lives actually would put the planes on a different crash course that pilots might not have time to recognize. "I thought I must have done something wrong," Platzer recalls. "I thought maybe I should go back to the drawing table and try to fix the mistakes in my program."
Platzer had come to Pittsburgh to work with world-renowned FORE Systems Professor of Computer Science Edmund M. Clarke, who holds a joint appointment in electrical and computer engineering. The following year, Clarke won the A.M. Turing Award from the Association for Computing Machinery—widely considered the Nobel Prize of computing—for his pioneering role in developing an automated method called model checking that finds design errors in computer hardware and software.
Model checking has transformed how the computer industry tests chips, systems, and networks, and it is now being used to debug applications, too. Computer scientists used to pore over lines of code manually, often in vain, to hunt for costly bugs. For instance, in 1994, a minor arithmetic glitch forced Intel Corp. to recall thousands of Pentium chips—a $500 million mistake.
Today, companies rely on model checking to catch such errors in hardware for everything from cell phones to external hard drives. Fast and automatic, model checking can verify highly sophisticated circuits with as many as 10120 configurations, a mind-boggling number equal to the numeral 1 followed by 120 zeroes. If there is an error, model checking will produce what's called a counterexample to reveal the source of the problem and provide important clues for how to repair it.
For all of its extraordinary power, model checking works best only with discrete systems—those with a finite number of possible configurations, such as a new circuit design for a computer microprocessor. It is more difficult to get the method right when analyzing what are called hybrid, or cyber-physical, systems.
As the name implies, cyber-physical systems are composed of both computerized and physical parts. Airplanes, for example, are cyber-physical systems. They move through the sky in physical space and also include computer controls that must make decisions in the face of constantly changing variables like shifting weather patterns and the movement of other planes in the sky.
Look around, Platzer says, and you will discover that we live in a world of cyber-physical systems, from cars and trains to robots and medical devices. The stakes are high in terms of both financial cost and human safety to make sure these systems work properly. Consider the recall of 8 million cars worldwide by Toyota since last fall because of reports that accelerator pedals can become stuck, possibly owing to a faulty electronics system.
"I am annoyed if my computer crashes, but I am really annoyed if my car crashes," says Platzer, who returned to Carnegie Mellon after earning his doctorate in 2008 and is now an assistant professor in the Computer Science Department. "So to a certain extent, it is much more important to get systems right that are actually interfacing with the physical environment and with humans because when they malfunction, it can be really dangerous."
Without model checking at their disposal, engineers do expensive trial-and-error testing and numerical simulation on computer-controlled devices such as automobiles and aircraft. "Yet, scary enough," Platzer notes, "it is obviously very difficult to test a system exhaustively."
Indeed, our powers of design now far outstrip our capacity to make sure the technologies we create will actually work properly in all possible real-world scenarios, according to Bruce Krogh, a professor of electrical and computer engineering at Carnegie Mellon, who also studies hybrid systems. "The problem," he says, "is how to ensure that you explore everything that can possibly happen, especially in large physical systems where the complexity becomes overwhelming."
He points to the catastrophe of USAir flight 427, which crashed in 1994 near the Greater Pittsburgh International Airport, killing all 132 people aboard. Investigations later showed that the aircraft's rudder became jammed, forcing the plane into an almost vertical roll less than 10 miles from the runway. "They determined that a mechanical system was able to get into a situation where controls from the pilot made it go exactly the wrong way," Krogh says. "I don't like dwelling on tragedies, but in all of the high-profile disasters like this, there is some situation that occurs that wasn't anticipated in testing or simulation."
However, as with the case of USAir 427, it's impossible to use model checking to examine every possible configuration of cyber-physical systems that must interact with the infinitely variable real world. These systems are highly nonlinear, meaning that small changes can have large effects, and their behavior often depends on more than a dozen variables. Model checking tools are still limited to handling problems with around four variables that are governed by more straightforward linear dynamics. "I cannot describe my car with that," Platzer says. "I'm not even sure if you can describe a coffee machine with that."
Ensuring that cyber-physical systems are free of potentially fatal errors is among the most difficult and important problems in computer science, agree experts, including Platzer, who was primed to take on this challenge at an early age. Ever since he was a young child growing up in Hamburg, Platzer has been interested in mathematics and logic. "The 'why' questions were most pressing for me as a boy," he recalls. "My parents still tell a lot of stories of me asking too many 'whys,' so I guess I had to end up as a scientist."
His first encounter with computers was in grade school when a geometry teacher required him to draw and measure hundreds of triangles to find the lengths of their missing sides. "I never really liked that, so I learned about trigonometric functions and wrote a computer program to do it for me," he recounts with a grin.
Platzer wasn't always focused on schoolwork. He had great success as a competitive ballroom dancer, even winning several major tournaments. He was so good at dancing it could've distracted him from his studies, but he decided to concentrate instead on computer science—and was accepted into 10 or so PhD programs after earning his master's degree from the University of Karlsruhe near the French-German border. "At some point you have to decide whether you want to do ballroom dancing professionally all the time, or do some research," he says. "Of course you can argue that flight choreography and dance choreography have some similarities. What you don't want are collisions, and what you do want are interesting maneuvers."
Platzer chose to join one of the biggest computer verification research projects in Europe at the University of Oldenburg, where he worked on a multi-institution initiative called Automatic Verification and Analysis of Complex Systems. Right away, he started asking more "why" questions. A self-described "logician," Platzer wondered why his colleagues weren't combining model checking with the principles of logic to verify the soundness of cyber-physical systems. "I wanted to know why we didn't have a nice logical language to state what we wanted a system to do," he says, "and then rove properties about whether it actually behaves in that way."
So with the same aplomb that it took to challenge his geometry teacher, Platzer set out to create just that. "A lot of people thought my idea couldn't possibly work—and even I thought there must be a reason why everyone does it differently, so why should it work?" he says.
Platzer developed an automated computer tool he named KeYmaera, a spin on the word "chimera," the fire-breathing beast in classical Greek mythology that was a hybrid of a lion's head, a goat's body, and a serpent's tail. It's an appropriate name for the first program to provide conclusive proof that hybrid systems will operate as intended—or else generate counterexamples to point out any flaws that might exist.
"It's a much more elegant, fundamental, and completely novel approach to something that has been worked on now for maybe 15 years," Carnegie Mellon's Krogh says. "André's research is still in its early stages, but it appears very promising for verifying systems where there are complex nonlinearities."
Using this logic-based approach, KeYmaera can check the reliability of systems with nonlinear dynamics and up to 40 variables—an order of magnitude improvement. And the applications are limitless because of the ubiquitous nature of cyber-physical systems in everything from pacemakers to power grids.
During his graduate years, Platzer applied the KeYmaera verification tool to check the reliability of the i-collision algorithms in the European Train Control System. The computerized system uses automated track sensors to prevent collisions of the high-speed bullet trains transporting millions of passengers daily throughout Europe. Platzer, following the logical point of view, determined that the system had to take into account the real-time movement of the trains, not just their anticipated timing.
"This was really the showcase scenario," Platzer says. "And it came as a great surprise to the people who know something about these kinds of systems that the answers I derived from logical approaches were much more complicated than what they expected."
But the real potential of KeYmaera became apparent when Platzer found a problem he wasn't even looking for when testing his program using the bank-right aircraft collision-avoidance maneuver as a benchmark. No matter how many times he checked the sound maneuver, he found certain angles that would cause planes to collide, rather than avoid a crash.
"On paper [the roundabout collision-avoidance protocol] looks terribly convincing, but for some strange configurations, this is exactly the wrong thing to do," Platzer says. "I kept thinking there was a way to fix it, but there never was. It was surprisingly broken."
Platzer's joint publication with Clarke on the flaws in the roundabout maneuver and their proposed bug-free fix won the Best Paper Award at last year's 16th International Symposium on Formal Methods—one of the most prestigious conferences in the field. The work also captured worldwide attention last October when Popular Science named Platzer to its annual Brilliant 10, a list of the brightest young researchers in the country. He became the fourth Carnegie Mellon faculty member to be named to the list, joining professors Carlos Guestrin (2008) and Luis von Ahn (2006), as well as Doug James (2005), now at Cornell.
The magazine dubbed the 31-year-old computer scientist as the "crash test anti-dummy," adding,"every now and then, an innovation so vital comes along that it's hard to imagine how we got along without it," the editors wrote, adding KeYmaera to a list of essentials like "seatbelts, antibiotics, [and] fire hoses."
Frank Pfenning, Carnegie Mellon professor of computer science and Associate Dean for Education in the School of Computer Science, taught a graduate-level logic course this spring with Platzer. He explains why his colleague's work has captured so much attention. "What you typically find is that people will make a practically important advance or someone will make a theoretical breakthrough," Pfenning says. "What you rarely ever find is someone at an early stage in their career who makes a deep theoretical advance that actually works for real problems."
Today, Platzer's phone rings with calls from automotive manufacturers, aircraft companies, and others interested in his technology. His vision is that KeYmaera—downloadable for free—will become an integral part of the product development process across many industries. As he works to scale-up his methods for widespread commercial use, Platzer is also among the researchers participating in the new Institute for Computational Modeling and Analysis of Complex Systems, a $10 million initiative headed by Clarke and funded by the National Science Foundation. The aim of the five-year program is to develop new computational tools to better understand complex systems ranging from the causes of pancreatic cancer to the operation of aircraft.
Although the practical applications of his research are exciting, Platzer is most eager to continue making fundamental advances in our understanding of hybrid systems. "During your PhD you have to focus on one thing, and you don't have the luxury of working on 10 exciting problems at once," he says. "Now I have this luxury again, but nevertheless, this is still the problem that is most fascinating to me."
He continues to await word that the FAA has scratched the proposed roundabout collision-avoidance maneuver from its Next Generation Air Transportation System. Thankfully, he says, overhauling the nation's air traffic control system is a slow, deliberate process. But Platzer wonders how many countless other bugs might be lurking undetected in safety-critical systems that have already been deployed.
In part, that's the reason he makes the 15-minute walk each morning to his office on the Pittsburgh campus. "When I walk, I can think," he says. "But when I drive, I better pay attention because otherwise all those automatic systems might not help me either."
For additional information:
Platzer Honored for Systems Research
