30 credits – Automated Annotation of Simulink Generated C Code Based on the Simulink Model

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.

Background:

In the domain of software engineering, model-based development (MBD) has proven to be an effective paradigm for developing complex software solutions.

Matlab Simulink is a de-facto standard MBD tool in automotive domain. Automotive engineers use Simulink to produce models that are executable specifications, that can be analyzed for correctness using different verification techniques, such as simulation and static analysis. Eventually, using specialized tools, the engineers can generate the operational C/C++ code which is deployed in vehicles. This automatically generated code still needs to be verified for correctness, preferably using formal verification techniques.

Target:

In this project, we would like to investigate how we can extract information from the Simulink models in order to automatically annotate the respective automatically generated code, such that it becomes suitable for verification using state-of-art deductive verification tools.

Assignment:

The project consists of three main activities:

  • Investigating whether there can be established an unambiguous (syntactic) relationship between the automatically generated C/C++ code and the Simulink models (find out which part of the Simulink models maps into a specific part of the generated C/C++ file)
  • Automatically extract verification annotations from the Simulink model and inject them into the generated C/C++ code. Validate this on a selected use-case from Scania.
  • Focus on the code generation tool that is currently used in Scania, with the possibility to investigate other tools (based on the number of students taking the project)
  • Education:

    Specify education or specialisation: This proposal is suitable as MSc thesis project. The candidates should have experience in Matlab Simulink and C/C++. Knowledge in deductive verification tools (VCC, Frama-C) is an advantage.

    Number of students: 1 or 2

    Start date: January/February 2020 or earlier depending on the availability of the selected candidates.

    Estimated time needed: 6 months

    Contact persons and supervisors:

    Mattias Nyberg, Technical Manager, 08-55383736Predrag Filipovikj, Postdoctoral Researcher, KTH and Scania

    .

    Skicka din ansökan till med rubrikraden Ny Teknik Jobb.

    Aktuellt inom