Safety Check

Andre Platzer

Driver assistance technologies, such as adaptive cruise control and automatic braking, promise to someday ease traffic on crowded routes and prevent accidents.

"Auto accidents cost society billions of dollars and too many lives, so automated systems that could increase both the safety and efficiency of our roads only make sense," said Andre Platzer, an assistant professor of computer science at Carnegie Mellon University.

But proving these automated systems will work as intended is a daunting task.

Platzer and his collaborators, Ph.D. students Sarah M. Loos and Ligia Nistor, have demonstrated it's possible to verify the safety of these highly complex systems.

They recently presented their findings at the International Symposium on Formal Methods, at the University of Limerick, Ireland.

The researchers first developed a model of a distributed car control system in which computers and sensors in each car combine to control acceleration, braking and lane changes, as well as entering and exiting the highway.

They then used mathematical methods to formally verify that the system design would keep cars from crashing into each other.

"The system we created is in many ways one of the most complicated cyber-physical systems that has ever been fully verified formally," said Platzer.

Formal verification methods are routinely used to find bugs in other computer circuitry and software.

In fact, Platzer is a leader in developing new techniques to verify complex computer-controlled devices such as aircraft collision avoidance systems and robotic surgery devices.

Using formal methods to either find errors in automated vehicle control or prove they are safe is particularly challenging, Platzer said.

They must take into account physical laws and the capabilities of the system's hardware and software.

But vehicle control systems add another layer of complexity because they are distributed systems.

That is to say, no single computer is ultimately in control; instead, each vehicle makes decisions in concert with other vehicles sharing the same road.

Platzer cautioned that their proof has a major limitation — it only applies to straight highway.

Addressing the problem of curved lanes, sensory inaccuracy and time synchronization are among the issues that will be a focus of future work.

The methods the CMU researchers developed can, however, be generalized to other system designs or to variations in car dynamics.

"Any implementation of a distributed car control system would be more complicated than the model we developed," Platzer said.

"But now at least we know that these future systems aren't so complex that we can't verify their safety."

This research was supported by the National Science Foundation and the Office of Naval Research.

Homepage Story Archives