Thesis Work 30hp Formal verification and validation for automotive specifications

A thesis project at Scania is an excellent way of making contacts for your future working life. Many of our current employees started their career with a thesis project.

Background:

Modern vehicles increasingly rely on computers and software to operate properly, and Scania is among the companies aiming to sell fully autonomous vehicles within the next few years. Therefore, the correctness of software at Scania, and in the automotive industry in general, is essential. Exhaustively verifying system correctness can be done using formal verification, which means using computer-assisted mathematical reasoning to prove that a system fulfills some formal specification. However, current methods for formal verification require significant time, resources and knowledge to apply, and have therefore not yet been widely adopted in the automotive industry. 

Target:

To formally verify vehicles, it is essential to have unambiguous and complete specifications represented in a mathematically rigorous way. Therefore, the goal of this project is to investigate how to state and prove specifications and to investigate different ways to represent specifications. For instance, it is often important to know whether a given specification is more restrictive than some other specification, or whether a specification is complete (covers all relevant cases or scenarios) with respect to some given conditions. Formal specification languages can also play a crucial role when combining different verification techniques.

Examples of assignment:

-    Define a formal language for specifications inside an interactive theorem prover (ITP) such as Isabelle/HOL, HOL4 or Coq
-    Use a formal specification language to formulate meaningful specifications for vehicles and their components inside an ITP
-    Define a custom deductive system inside an ITP to formally reason about specifications 
-    Use a custom deductive system inside an ITP to formally prove non-trivial relationships between specifications
-    Investigate methods to validate specifications (e.g., on completeness)
-    Investigate flowgraphs as a representation for the purpose of formal reasoning
-    Conduct case studies to evaluate different methods and tools for verification and validation of specifications

We are also interested in hearing other ideas for directions of the thesis, which can be discussed before the start to better match the applicant’s interest and background.

Education:

M.Sc. in Engineering or similar with an interest in computer science, formal methods, or interactive theorem proving.

Contact person and supervisor:
Anton Hampus, PhD student, +46737787449, anton.x.hampus@scania.com
Mattias Nyberg, Adj. prof, KTH / Research Manager, Scania, mattias.nyberg@scania.com

Number of students: 1-3
Time:20 weeks, full time 40 hours per week
Start: Jan 2025
Credits: 30hp
 
Application:
Enclose CV, personal letter and transcript of grades.
 
A background check might be conducted for this position. We are conducting interviews continuously and may close the recruitment earlier than the date specified.