Publication

This paper presents a method for formal verification of automotive collision avoidance systems. Using viability theory and reachability analysis, we define when the system should intervene, i.e. the unsafe set, and when the system should not intervene, i.e. the safe set. Given these sets, we formulate the problem of verifying that a given system does not make incorrect decisions as an optimization problem. The method is demonstrated on a collision avoidance system example and, given the models used and absence of measurements errors, we show that the system does not make incorrect decisions. Furthermore, we describe and demonstrate how to evaluate the robustness to measurement errors, using the proposed framework.