Verification of Intelligent Driving Systems

Abstract:

Automotive applications require an exceptionally high level of confidence. For instance, the faulty ignition switches in General Motors vehicles have resulted in 52 crashes and at least 2.6 million vehicles with these switches have been recalled. If each vehicle spent only 1,000 hours on the road, there has been less than 1 crash every 5 x 107 hours of operation. Test tracks and simulations are unable to reliably detect failures that occur this infrequently. It is unreasonable to expect individual mechanical devices to have levels of failure as low as needed in automotive applications. The crashes occurred because of the interaction between the switch and the steering and braking systems. When the ignition was turned off while the vehicle was in motion, the other systems should not have been disabled. This is a protocol issue, which could have been predicted by protocol verification techniques developed at Bell Labs. In the 1990's probabilistic verification techniques were developed that guaranteed that the protocols used in the telephone network had extremely low probabilities of failure. This technique can provide the level of confidence required in new intelligent driving applications, but cannot be applied directly because of the complexity of these applications. 1) Intelligent driving applications interact with the physical world in multiple ways, while communications protocols only interact with the physical world over the communications channel. Each interaction has its own failure modes. 2) Vehicles execute time-critical actions, such as braking or merging. The time dimension makes protocols much more difficult to model and analyze. And, 3) intelligent driving applications may require interactions between large numbers of vehicles, while most of the communications systems that have been verified only have two participants. The composite state space that describes the possible interactions between participants following a protocol grows exponentially with the number of participants. We have resolved the complexity issues by: 1) Developing a multiple stack, layered architecture. Each interaction with the physical world has its own stack, with the interaction with the physical world at the lowest layer and the cyber operations in the higher layers. This is similar to the layered architecture used in communications networks, and allows the layers to be modified and verified separately. Our strategy for the interactions between the stacks disallows protocol loops. 2) We have synchronized the clocks and separated time and logical operations into different stacks. The separation allows the verification of timing constraints, resulting from the physical operation of an automobile, and the verification of the logical operations to be conducted by different techniques. Synchronized clocks permit vehicles to simultaneously perform operations, which reduces the number of possible sequences of events. Synchronized clocks have also provided unique guarantees for a lock protocol and a broadcast protocol. And, 3) we have improved the calculation of the bounds on failure probabilities. Probabilistic verification checks the most likely sequences of events first, up to the memory and time limits of a computer system. At the end of a verification, the number of unexplored paths are counted and an upper bound on failures is determined. The bound has been tightened, by orders of magnitude in some cases, by solving a linear program that determines the probability of reaching unexplored states. The verification techniques have been applied to a lock protocol that uses synchronized clocks and a driver assisted merge protocol that creates gaps in the flow of traffic and informs drivers when it is safe to change lanes.