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

Sodertalje, Stockholm
den 19 september 2019
den 2 december 2019
Övriga jobb
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.

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.

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.

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

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


Enclose CV, personal letter and school-leaving certificate .

Scania är en världsledande leverantör av transportlösningar. Tillsammans med våra partners och kunder driver vi omställningen till ett hållbart transportsystem. 2018 levererade vi 88 000 lastbilar, 8 500 bussar samt 12 800 industri- och marinmotorer till våra kunder. Nettoomsättningen uppgick till mer än 137 miljarder kronor, varav cirka 20 procent var tjänsterelaterade. Scania grundades 1891 och är idag verksamt i fler än 100 länder och har cirka 52 000 medarbetare. Forskning och utveckling är koncentrerad till Sverige, med filialer i Brasilien och Indien. Tillverkning sker i Europa, Latinamerika och Asien, med regionala produktionscentrum i Afrika, Asien och Eurasien. Scania är en del av TRATON SE. För mer information besök:

Liknande jobb

Liknande jobb