Bug-free Self-Drive: Distributed Car Control System Verified Safe

Driver assistance technologies predict to ease traffic on crowded routes and prevent accidents someday. Proving that these automated systems such as adaptive cruise control and automatic braking will work as intended is an intimidating task, but computer scientists at Carnegie Mellon University have now demonstrated it is possible to verify the safety of these highly complex systems. In order to do so, the researchers first formulated a model of distributed car control system in which sensors and computers in each car, coalesce to control acceleration, brake and lane changes, in addition to entering and exiting the highway. Then mathematical methods were incorporated to formally verify that the system configuration and design will prevent the cars from crashing into each other.

#-Link-Snipped-#
Bug Free Self Drive

Andre Platzer, an assistant professor of computer science said, “The system we created is in many ways one of the most complicated cyber-physical systems that has ever been fully verified formally.” The findings were presented at the International Symposium on Formal Methods, June 22 at the University of Limerick, Ireland, by Platzer and his collaborators, Ph.D. students Sarah M. Loos and Ligia Nistor. Platzer added, "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, It would be foolish to move to such a system, however, unless we can be certain that it won't create problems of its own. The dynamics of these systems have been beyond the scope of previous formal verification techniques, but we've had success with a modular approach to detecting design errors in them."

Platzer is a leader in formulating new techniques to verify complex computer-controlled devices like aircraft collision avoidance system and robotic surgery devices, physically known as cyber-physical systems or hybrid systems. He has also applied various formal verification methods to routinely detect bugs in computer circuitry and software. Besides, he is a member of the Computational Modeling and Analysis of Complex Systems (CMACS) center, a CMU-based initiative sponsored by the National Science Foundation to apply verification techniques to a variety of complex biological or physical systems.

Platzer said, “using these formal methods to either find errors in automated vehicle control or prove they are safe is particularly challenging. Like other cyber-physical systems, they must take into account both 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, no single computer is ultimately in control, but rather each vehicle makes decisions in concert with other vehicles sharing the same road.”

Platzer, Loos and Nistor demonstrated that they could affirm the safety of their adaptive cruise control system by breaking the problem into modular pieces and organizing the pieces in a hierarchy. The smallest piece comprises of just two cars in a single lane. Establishing on that, they were able to prove that the system is safe for a single lane with an arbitrary number of cars, and ultimately for a highway with an arbitrary number of lanes. Similarly, they were able to show that cars could safely merge in and out of a single lane and then extended it to prove that cars could safely merge across a multi-lane highway.

Platzer admonished that this 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 Carnegie Mellon researchers developed can, however, be generalized to other system designs or to variations in car dynamics.

Platzer said, "Any implementation of a distributed car control system would be more complicated than the model we developed,but now at least we know that these future systems aren't so complex that we can't verify their safety."

National Science Foundation and the Office of Naval Research were a few supporters supporting this research.

Source: #-Link-Snipped-#