Driver assistance technologies, such as adaptive cruise control and automatic braking, promise to someday ease traffic on crowded routes and prevent accidents. Proving that these automated systems will work as intended is a daunting task, but computer scientists at Carnegie Mellon University have now demonstrated it is possible to verify the safety of these highly complex systems.
To do so, 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 Andre Platzer, an assistant professor of computer science. He and his collaborators, Ph.D. students Sarah M. Loos and Ligia Nistor, will present their findings at the International Symposium on Formal Methods, June 22 at the University of Limerick, Ireland.
"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," Platzer said. "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."
Formal verification methods are routinely used to find bugs in computer circuitry and software; Platzer is a leader in developing new techniques to verify complex computer-controlled devices such as aircraft collision avoidance systems and robotic surgery devices, known collectively as cyber-physical systems, or hybrid systems. He also 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.
Using these formal methods to either find errors in automated vehicle control or prove they are safe is particularly challenging, Platzer said. 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 showed that they could verify 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 consists of just two cars in a single lane. Building 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. Likewise, 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 cautioned 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.
"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. Follow the Carnegie Mellon School of Computer Science on Twitter @SCSatCMU.
About Carnegie Mellon University: Carnegie Mellon (www.cmu.edu) is a private, internationally ranked research university with programs in areas ranging from science, technology and business, to public policy, the humanities and the arts. More than 11,000 students in the university's seven schools and colleges benefit from a small student-to-faculty ratio and an education characterized by its focus on creating and implementing solutions for real problems, interdisciplinary collaboration and innovation. A global university, Carnegie Mellon's main campus in the United States is in Pittsburgh, Pa. It has campuses in California's Silicon Valley and Qatar, and programs in Asia, Australia, Europe and Mexico. The university is in the midst of a $1 billion fundraising campaign, titled "Inspire Innovation: The Campaign for Carnegie Mellon University," which aims to build its endowment, support faculty, students and innovative research, and enhance the physical campus with equipment and facility improvements.
Byron Spice | EurekAlert!
New algorithm for optimized stability of planar-rod objects
11.08.2016 | Institute of Science and Technology Austria
Automated driving: Steering without limits
05.02.2016 | FZI Forschungszentrum Informatik am Karlsruher Institut für Technologie
Researchers from the Institute for Quantum Computing (IQC) at the University of Waterloo led the development of a new extensible wiring technique capable of controlling superconducting quantum bits, representing a significant step towards to the realization of a scalable quantum computer.
"The quantum socket is a wiring method that uses three-dimensional wires based on spring-loaded pins to address individual qubits," said Jeremy Béjanin, a PhD...
In a paper in Scientific Reports, a research team at Worcester Polytechnic Institute describes a novel light-activated phenomenon that could become the basis for applications as diverse as microscopic robotic grippers and more efficient solar cells.
A research team at Worcester Polytechnic Institute (WPI) has developed a revolutionary, light-activated semiconductor nanocomposite material that can be used...
By forcefully embedding two silicon atoms in a diamond matrix, Sandia researchers have demonstrated for the first time on a single chip all the components needed to create a quantum bridge to link quantum computers together.
"People have already built small quantum computers," says Sandia researcher Ryan Camacho. "Maybe the first useful one won't be a single giant quantum computer...
COMPAMED has become the leading international marketplace for suppliers of medical manufacturing. The trade fair, which takes place every November and is co-located to MEDICA in Dusseldorf, has been steadily growing over the past years and shows that medical technology remains a rapidly growing market.
In 2016, the joint pavilion by the IVAM Microtechnology Network, the Product Market “High-tech for Medical Devices”, will be located in Hall 8a again and will...
'Ferroelectric' materials can switch between different states of electrical polarization in response to an external electric field. This flexibility means they show promise for many applications, for example in electronic devices and computer memory. Current ferroelectric materials are highly valued for their thermal and chemical stability and rapid electro-mechanical responses, but creating a material that is scalable down to the tiny sizes needed for technologies like silicon-based semiconductors (Si-based CMOS) has proven challenging.
Now, Hiroshi Funakubo and co-workers at the Tokyo Institute of Technology, in collaboration with researchers across Japan, have conducted experiments to...
14.10.2016 | Event News
14.10.2016 | Event News
12.10.2016 | Event News
21.10.2016 | Health and Medicine
21.10.2016 | Information Technology
21.10.2016 | Materials Sciences