Managing Complexity in Safe Lane Merging Protocols

Abstract:

We are designing lane merging systems that assist drivers to maneuver safely. The driver signals his intent to change lanes. The cars communicate and create a safe gap. The driver is notified when it is safe to merge, or when a condition occurs that makes a lane change dangerous. The protocols coordinate the merge over an unreliable channel, they use sensors that may be inaccurate, they control the speed and braking of vehicles with different operating characteristics, and there may be interference with vehicles that are not participating in the protocol, other obstacles in the environment, and unexpected maneuvers by the drivers of the collaborating vehicles.
Our objective is to design protocols that will not cause an accident for all possible combinations of equipment failures and interference. Collaborative driving systems are among the most complex that we have encountered. Failure to design safe systems may be measured in lost lives. Engineering is the art of managing complexity. We are investigating three techniques to manage the complexity of these systems. In our next project we are reducing these techniques to practice, and generalizing them to other cyber--physical systems.
The techniques include:

• A multi--dimensional, stack architecture.
• Synchronized clocks.
• A multi--manufacturer verification technique that decomposes verification into model checking and conformance testing.
• There is a dimension for each interaction with the physical world, and a dimension for the applications. Each dimension is organized as a stack, similar to the stack architecture used in communications. The architecture separates the physical properties of the dimension from the logic in an intelligent application. Each layer of a stack provides well defined services over well defined interfaces.
• We can prove that a layer provides a service, assuming that the services provided by a lower layer have been verified. In the merge protocol we prove that the merge protocol is safe assuming that an intelligent cruise control protocol, in a lower layer, can create and maintain a gap that is specified.

We can change the operation of any layer without changing the other layers. The communications stack has made it possible to change the transmission technologies in the Internet without changing the email application. In CPS systems we may even be able to reuse entire stacks in different applications. For instance, the communications stack and timing stack provide services that are likely to be the same in all collaborative CPS systems. The parts of the sensor stack that merge the sensors form different participants may also be re--used in other CPS applications. Timers that are initiated over an unreliable communications channel, which may require several transmissions before a message is received, can result in multiple execution sequences. The larger the number of possible execution sequences, the more difficult it becomes to prove that all of the sequences are correct. Synchronized clocks reduce the number of execution sequences by specifying the time that an operation is performed, rather than initiating timers at uncertain starting times. Clocks can be accurately synchronized using GPS, when GPS isn't available for short amounts of time, they can be maintained with crystal oscillators, and when GPS isn't available for long periods of time, local clocks can be synchronized using NTP. Intelligent automobiles must be able to collaborate safely with all of the other intelligent automobiles on a highway. Testing all combinations of implementations, for all of the automobile manufacturers, all of their different models, and all of the different model years can result in very large numbers of tests. We are investigating a strategy that we used to test telephone equipment after the telephone network was opened to competition. We create an unambiguous, formal model of a protocol and verify that the model provides a safe service. We then generate a black box test sequence to determine if an implementation correctly and completely implements the model. The black box test sequence applies a set of inputs to the implementation and observes the outputs. If an implementation passes the tests, it will interoperate with all of the other implementations that pass the test. We have successfully generated tests for communications equipment that is not heavily dependent on time. We are investigating applying the test generation procedures to CPS systems that are time critical, but use synchronized clocks and store the deadlines for all of the participants in a replicated memory.