Automatically Assessing Correctness of Autonomous Vehicles Auto-CAV

Purpose and goal

The project aimed to establish formal methods as an efficient tool in the development of safety-critical software for automated vehicles. The overall goal was to address the challenges in the development and verification of safe automated driving systems, thereby contributing towards achieving safer vehicles and improved traffic safety. The results and insights obtained from the project are documented in several academic publications including a Licentiate thesis and a PhD thesis.

Expected results and effects

Several formal methods to model, specify, and verify automated driving systems are evaluated. Insights into how the evaluated methods differ and the challenges involved are documented and published. Formal modelling guidelines and methods to identify and address subtle modelling errors are developed. A systematic approach to automatically obtain formal models is developed and validated by a proof of concept. A structured approach on how to use various formal artefacts to provide evidence for safety arguments of automated driving systems is also published.

Planned approach and implementation

The project has been run as an industrial PhD project in collaboration with Zenseact (formerly Zenuity) and Chalmers University of Technology. The research is motivated by industrial need and therefore the problem statements, research questions, methods and the results are closely coupled with the industrial research and development of automated driving systems. A significant part of the research method in this project involves mathematical modelling and mathematical proofs.