Course paper / final thesis

Model Checking On-Board Computer Network

Starting date

1 May 2017

Duration of contract

3 to 6 month depending on university requirements

Type of employment


Your mission:

The mission of the DLR Simulation and Software Technology is to support spacecraft engineering with new technology and innovative software.

In the project “Scalable On-Board Computing for Space Avionics” (ScOSA), we are developing a distributed, reliable and reconfigurable on-board computer for future space missions. In this system, different software tasks run on different processor nodes and exchange messages. In case of a failure, the system should be able to detect it and reconfigure itself.

In order to increase our confidence in the system, we would like to analyze it using formal techniques such as model checking. We are interested in questions like: Can the system detect a fault within the given time? Will the critical message be delivered within the given time bounds? Is it possible that multiple reconfigurations are triggered simultaneously?

The goal of this work is to evaluate the capabilities of existing model checking tools and approaches, identify properties of interest that can be checked for ScOSA, and get some insight into the system sizes for which model checking is practical.

As part of this project you will work on following tasks:

  • Evaluate existing model checkers
  • Create models of the network and traffic within it using state machines or other appropriate formalisms
  • Perform model checking experiments on the created models
  • Ideally, integrate the results into our software framework “Virtual Satellite”

If you would like to take on this challenging task, we are looking forward to receiving your application.

Your qualifications:

  • you are currently doing your Master’s course in computer science or mathematics
  • you are interested in applying formal methods (in particular, model checking) to real projects
  • ideally, you already have some theoretical background in formal methods
  • ideally, you have some experience in software development with Java
  • you are able to communicate in English (the supervision will be in English)

Your benefits:

Look forward to a fulfilling job with an employer who appreciates your commitment and supports your personal and professional development. Our unique infrastructure offers you a working environment in which you have unparalled scope to develop your creative ideas and accomplish your professional objectives. We are striving to increase the proportion of female employees and therefore particularly welcome applications from women. Disabled applicants with equivalent qualifications will be given preferential treatment.

Technical contact

Philipp Martin Fischer
Simulations- und Softwaretechnik

Phone: +49 531 295-2951

Send message

Vacancy 06593

HR department Braunschweig

Send message

DLR site Braunschweig

To location

DLR Simulations and Software Technology

To institute