Thesis work 30hp - Formal verification of software over real-time properties

Ingress:

Thesis work is an excellent way to get closer to Traton and build relationships with industries for the future. Many of today's employees began their Scania/Traton career with their degree project.

Background:

Modern automotive systems depend on increasingly large and complex software. The demand for reliable, safe, and efficient code is rising as functionality grows. In safety-critical systems, demonstrating software safety requires significant testing effort. However, testing alone cannot guarantee that all possible system behaviours meet safety requirements.

Formal verification provides an alternative approach, where a model of the software is built and its correctness is proven mathematically with respect to a formal specification. In embedded automotive systems, temporal behaviour is a key concern: correctness depends not only on what the software computes, but also on when these computations occur. Verifying that real-time temporal specifications are met is therefore crucial for ensuring the correctness of embedded software.

Target:

The goal of this project is to explore and evaluate methods for specifying and verifying real-time properties of embedded software using formal methods. The focus is on assessing how these techniques can be applied in an industrial setting for automotive embedded systems.

Example assignments:

· Explore methods to specify and formalize real-time properties for industrial embedded software.

· Develop approaches to construct monitors for temporal properties and evaluate their use in verifying embedded software with model checkers.

· Compare different tools and techniques for the verification of real-time temporal properties.

Education:

Education: MSc in Computer Science or similar, with some background in formal methods.

Number of students: 1.

Start date: January/February 2026.

Estimated time needed: 20-25 weeks.

Contact person and potential supervisor:

Gustav Ung, Industrial Ph.D. student, KTH / Traton,

gustav.ung@se.traton.com 

Recruiting Manager: Elvedin Ramic,

elvedin.ramic@scania.com

Application:

Enclose CV, personal letter and transcript of records.

A background check might be conducted for this position. We are conducting interviews continuously and may close the recruitment earlier than the date specified.