30hp – Formally proving correctness of architectural framework to support development of safety critical systems i Sodertalje

Scania genomgår nu en transformation från att vara en leverantör av lastbilar, bussar och motorer till en leverantör av kompletta och hållbara transportlösningar.

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.

Development of complex systems such as autonomous vehicles requires the usage of an architectural framework. In such an architectural frameworks, fundamental artifacts such as “system”, “program”, “signal”, and “interface” are defined. To support development of safety critical systems, the correctness and consistency of the architectural framework needs to be ensured; i.e. the framework needs to be formally verified.

Formal techniques to prove correctness of individual artefacts are gaining interest, e.g. proving correctness of source code. In this MSc project, the goal is to use such formal techniques to obtain mathematical proofs of the correctness and consistency of an architectural framework that has previously been developed by Scania in collaboration with KTH.

The architectural framework used by Scania has already been formulated in terms of mathematical definitions and theorems. Informal proofs are also available for many of the theorems. The main task of the thesis is to write and check these proofs using a proof assistance systems, such as Coq, Agda, Isabelle, Mizar, MetaMath.

1. Study literature on architectural frameworks and their formalizations, including Scania’s.
2. Create an overview of proof assistance systems.
3. Select one or two proof assistance systems.
4. Write some selected proofs in the selected proof assistence systems.
5. Evaluate and give recommendations on usage of proof assistance systems for verifying architectural frameworks.

Specify education or specialization: M.Sc. in computer science, mathematics, control theory, applied physics, or electrical engineering. Important is a strong interest in mathematics.

Number of students: 1-2.

Start date: January/February 2019.

Estimated time needed: 6 months.

PhD Mattias Nyberg, technical manager, 08-553 83 736, .

PhD Jonas Westman, systems engineering information and tools