Holistic Synthesis and Verification for Safe and Secure Autonomous Vehicles

The automotive industry is one of the most important industries in Sweden. With the development of AI technologies, autonomous driving (AD) functions are gradually deployed in modern vehicles, such as Autopilot in Tesla cars. However, no matter what the companies claim, the current AD functions actually require full or active supervision of human drivers, which makes the solution not fully autonomous. One of the obstacles that hinder the realization of AD is safety and security. In a fully autonomous vehicle, human drivers cannot be counted on to handle exceptional situations, which means the AD controllers must take full responsibility for any software or hardware errors. However, despite the crucial responsibility and high importance of AD controllers, the most common techniques are either a simple cycle of trial-error-trial or dependent on manual analysis, e.g., fault-tree analysis (FTA).

Additionally, security issues have emerged in recent years, and the problem has become even worse in the context of AD vehicles because most of them are interconnected or connected to cloud-computing servers. An security attack on the control software or embedded database of the vehicle would influence the safety of the system. Hence, the co-design and verification of safe and secure AD controllers are an urgent need for the automotive industry. However, there are many challenges in the synthesis and verification of safe and secure AD controllers and the goal for this project is to overcome these challenges. Briefly, the challenges that are addressed in the project are i) heterogeneity of AD controllers, ii) co-engineering of safety and security functions, iii) synthesis of AD controllers, and iv) trustworthy machine learning in AD. To address those challenges, we will propose a framework that considers the synthesis and verification of safe and secure AD controllers holistically.

The framework will be based on the state-of-the-art (SOTA) formal methods, such as probabilistic model checking, and the most advanced machine-learning techniques, such as large language models (LLM), and it will integrate the existing tools that are used in the industrial partners, such as fault-tree analysis, and the SOTA tools/methods, which will improve the performance of the existing tools and the quality of the AD functions that are deployed in their products. Most importantly, the research results of this project will advance the SOTA in the following aspects: i) the controller synthesis and verification algorithms will be scalable for industrial problems, which are not fully solved in the community of formal methods, ii) the framework that incorporates the algorithms will support the co-design and verification of both safety and security of the system, and iii) the gap between formal methods community and practitioners who have limited knowledge about formal methods will be bridged by our LLM-powered tool in the context of AD controller synthesis and verification.

Project objective

The project goal is to overcome the main challenges of synthesis and verification of safe and secure AD controllers, which exist in the current automotive industry in Sweden.

OB1. A systematic evaluation of the advanced techniques of synthesis and verification, obtaining their strengths and weaknesses in the development of safe and secure AD controllers. OB2. A framework for the synthesis and verification of safe and secure AD controllers. The framework must be able to recognize various modelling languages and support formal verification of these models, and the database for AD controllers must have a security guarantee. OB3. A methodology for realizing safe and secure ML-trained AD controllers. We aim to develop a new methodology that combines the state-of-the-art tools/methods (identified in OB1) and the existing tools/methods used in the industrial context. OB4. An evaluation of the framework (OB2) that incorporates the new methodology (OB3) through case studies and experiments in industrial environments.