Formal Validation of Probabilistic Collision Risk Estimation for Autonomous Driving

Autonomous driving technology is rapidly advancing towards level 5 autonomy along with claims of increasing safety on roads. However, a proper validation of such safetycritical, complex systems and of their reliability still needs to be addressed adequately. To this end, standard exhaustive methods are inappropriate to validate the probabilistic algorithms widely used in this field and new solutions need to be adopted. In this work, we present a new approach where formal verification is employed to validate systems with probabilistic predictions. In particular, we focus on the risk assessment generated by a probabilistic perception system, the Conditional Monte Carlo Dense Occupancy Tracker (CMCDOT). This framework provides an environment representation through Bayesian probabilistic occupancy grids and estimates Time-to-Collision probabilities for every static and dynamic part of the grid in near future. Focusing on the validation of the probabilistic collision risk estimation, we adopt the CARLA simulator to generate a large number of realistic intersection crossing scenarios with two vehicles. The formal verification is then performed using the XTL model checker of the CADP toolbox, based on the definition of appropriate Key Performance Indicators (KPIs). Finally, a quantitative analysis that goes beyond classical temporal logic verification is provided.