30 Credits – Formal Verification of Simulink Models Using Bounded Model Checking

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:

Formal verification represents an umbrella term that includes a set of verification techniques based on rigorous mathematical principles that can be used to show that a given system (model) behaves according to its specification.

As the vehicular systems have become increasingly complex, the need for applying rigorous verification techniques for showing the correctness of the automotive software has been highly recommended by safety regulatory bodies (ISO26262). However, application of such verification techniques is still not in a production phase, consequently, industry is partnering with academia to investigate the applicability of such verification techniques on running software models.

Target:

The intended purpose of this project is to apply a state-of-art formal verification technique, namely bounded model checking (BMC) and a novel research tool called SYMC on a selected use-case Simulink model from Scania, to verify its correctness with respect to safety properties.

The tool has already been applied on an industrial use-case for verification of safety requirements, namely the Brake-by-Wire system from Volvo GTTT with encouraging results. In this thesis project, we aim to extend the boundaries of applicability of the given technique and tool for verification of safety properties by applying it on another operational Simulink model from Scania.

Assignment:

The thesis includes, but is not limited to the following activities:

  • Preprocess a given Simulink model into formal suitable to be used as an input into SYMC tool
  • Apply the SYMC tool to verify safety and liveness properties
  • This might potentially require the student(s) to contribute in the codebase of the SYMC tool 
  • Education:

    Specify education or specialization: M.Sc. in Engineering or similar, with an interest for mathematics and formal verification. This thesis requires background in Matlab Simulink. Knowledge in Python is considered an advantage.

    Number of students: 1-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-55383736

    Predrag Filipovikj, Postdoctoral Researcher, KTH and Scania

    Application:

    Enclose CV, personal letter and school-leaving certificate

    .

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

    Aktuellt inom