SATISFIES

GOAL: Overcome the challenges of synthesis and verification of safe and secure autonomous driving (AD) controllers.

• Safety: AD vehicles do not damage objects in the environment, like pedestrians, and itself.

• Security: AD vehicles do not get damaged by external intruders, like cyber attacks.

• Verification: Existing AD controllers are guaranteed to be functionally correct, safe, and secure.

• Synthesis: To generate new AD controllers that are functionally correct, safe, and secure.

Abstract: 

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. A 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.