A Case Study on Using Probabilistic Verification to Find Failures in a Cooperative Driving Application

This paper introduces techniques that help proving the safety of cooperative driving applications. Most automotive applications are evaluated by means of simulations and test tracks, which cannot provide the degree of confidence that is demanded by the driving public. We introduce probability verification as an evaluation tool that provides greater degree of confidence over safety. This technique is applicable to systems with large state spaces that cannot be exhaustively verified by other model checking techniques. We present a protocol that assists drivers in merging between other vehicles. The protocol is built on a multiple stack architecture that partitions the system into smaller manageable components that can be tested and verified individually. A module is verified assuming that the modules that it depends on have been verified. The modules in different vehicles use synchronized clocks to reduce the number of states needed to be examined in the composite protocols that describe their interactions. We are able to show that system failures will occur with a sufficiently small probability. Since probabilistic verification is also used to verify the operation of the modules that provide services, the residual probability of failure of these modules must be considered in the probabilistic verification of any module.