Bachelor and Master Theses

Background

Simulation-based testing plays an important role in the validation and verification of automated vehicles. To generate various scenarios for simulation, State-of-the-art approaches first formulate a scenario space (e.g., all possible cut-in scenarios) into a parameter space based on a list of unrealistic assumptions (e.g., the cut-in vehicle drives with a constant speed before cutting in.)  On the one hand, synthesizing scenarios directly from formal specifications can remove the reliance on those unrealistic assumptions. It also provides a more flexible way to describe scenarios. On the other hand, when having traffic logs, searching the wanted scenarios in the logs can also benefit from formal methods.

In this project, the student will study formal modelling, formal verification, and reinforcement learning in a state-of-the-art model checker, UPPAAL. The student will use Python as the main programming language to construct, configure, and generate scenarios. CommonRoad is another platform that the student is going to study and use to visualise scenarios.

Objective

In this work, the students will study the symbolic model checking and synthesis techniques in UPPAAL and apply them in scenario generation and scenario matching for autonomous vehicles. In the work of scenario generation, the student will work on building formal models of vehicles and environment, and use model checking and reinforcement learning to generate various scenarios. In the work of scenario matching, the student will work on searching the traffic logs and finding wanted scenarios, such as cut-in and cut-out.

The students will work on potential problems in several aspects, e.g., scalability, complexity, and automation. A tool based on Python, UPPAAL, and CommonRoad is expected to be designed and implemented, which is able to generate various scenarios for testing a function of autonomous vehicles, such as cut-in or cut-out.

Job description

The students need to conduct a literature study to understand the state of the art in this area.

The students need to study UPPAAL and the model checking and synthesis techniques in UPPAAL and understand their strengths and limitations.

Case study: The students need to try their solution on a cut-in scenario.

The students need to summarize their work into a technical report and present the result.

Education/program/focus

Indicate education, program or focus: computer science, software engineering, embedded systems or other relevant programs

Start date for the thesis work: Autumn 2025

Estimated time required: 20 weeks

Contact persons and supervisors

Rong Gu, rong.gu@mdu.se  

Addition:

Good candidates will be recommended to conduct the study in Scania.