Facilitating Formal Verification of Cooperative Driving Applications

The next generation of intelligent vehicles will evolve from being able to drive autonomously to ones that communicate with other vehicles and execute joint behaviors. Before allowing these vehicles on public roads, we must guarantee that they will not cause accidents. We will apply formal methods to ensure the degree of safety that cannot be assured with simulation or closed-track testing. However, there are challenges that need to be addressed when applying formal verification techniques to cooperative driving systems. This thesis focuses on the techniques that address the following challenges: 1. Automotive applications interact with the physical world in different ways; 2. Cooperative driving systems are time-critical; 3. The problem of state explosion when we apply formal verification to systems with more participants. First, we describe the multiple stack architecture. It combines several stacks, each of which addresses a particular way of interaction with the physical world. The layered structure in each stack makes it possible for engineers to implement cooperative driving applications without being bogged down by the details of low-level devices. Having functions arranged in a layered fashion helps us divide the verification of the whole system into smaller subproblems of independent module verification. Secondly, we present a framework for modeling the protocol systems that uses GPS clocks for synchronization. We introduce the timing stack, which separates a process into two parts: the part modeled as an finite-state machine that controls state transitions and messages exchanges, and the part that determines the exact moment that a timed event should occur. The availability of accurate clocks at different locations allows processes to execute actions simultaneously, reducing interleaving that often arises in systems that use multiple timers to control timed events. With accurate clocks, we create a lock protocol that resolves conflicting merge requests for driver-assisted merging. Thirdly, we introduce stratified probabilistic verification that mitigates state explosion. It greatly improves the probability bound obtained in the original probabilistic verification algorithm. Unlike most techniques that aim at reducing state space, it is a directed state traversal, prioritizing the states that are more likely to be encountered during system execution. When state traversal stops upon depleting the memory, the unexplored states are the ones that are less likely to be reached. We construct a linear program whose solution is the upper bound for the probability of reaching those unexplored states. The stratified algorithm is particularly useful when considering a protocol system that depends on several imperfect components that may fail with small but hard-to-quantify probabilities. In that case, we adopt a compositional approach to verify a collection of components, assuming that the components have inexact probability guarantees. Finally, we present our design of driver-assisted merging. Its design is reasonably simplified by using the multiple stack architecture and GPS clocks. We use a stratified algorithm to show that merging system fails less than once every 5 × 10¹³ merge attempts.