Unternehmen suchen nach Dir. LASS DICH JETZT FINDEN!

Generierung von Inputsequenzen zum Test und zur Analyse von Monitor-Spezifikationen (m/w)

Deutsches Zentrum für Luft- und Raumfahrt (DLR)
Braunschweig

Top
Job-Infos

Berufsfelder

  • Anwendungsentwicklung

Gewünschte Studienfächer

  • Informatik
  • Ingenieurwissenschaften
  • Mathematik

Abschluss

  • Bachelor
  • Master/Diplom

Einsatzorte

  • Braunschweig

Fähigkeiten

  • C++
  • Java
  • Python
Stellenbeschreibung

Ihre Mission:

Unbemannte Luftfahrzeuge sind hoch komplexe und sicherheitskritische Systeme. Der Nachweis, dass diese Systeme korrekt in allen möglichen Situationen funktionieren ist ein wichtiges jedoch bisher ungelöstes Problem. Statische Analyseverfahren stoßen hierbei an ihre Grenzen. Ein Lösungsansatz ist es, nicht nachweisbare Eigenschaften zur Laufzeit kontinuierlich zu überwachen.  Dabei wird explizit geprüft, ob die erzeugten Daten des Systems den Erwartungen entsprechen. Die Erwartungen werden zuvor spezifiziert. Um komplexe Zusammenhänge der einzelnen Datenflüsse auszudrücken und später zu überwachen eignen sich insbesondere formale Spezifikationssprachen. Sie bieten die Möglichkeit temporale Kausalitäten der erzeugten Systemdaten auf eine modulare Weise auszudrücken und aus der Spezifikation heraus einen Monitor zu synthetisieren. Folglich ist eine korrekte Spezifikation als auch eine korrekte Synthese des Monitors entscheidend.

Im Rahmen dieser Arbeit sollen Inputsequenzen anhand einer formalen Spezifikationssprache erzeugt werden. Als Werkzeug können hierbei existierende SMT- oder SAT- Solver genutzt werden. Das Ergebnis dieser Arbeit ist sowohl relevant für die Validierung einer Spezifikation als auch für das Testen des synthetisierten Monitors. Die  generierten Sequenzen können als Input für den Monitor genutzt werden, um eine erhöhte Testabdeckung zu gewährleisten. Die temporalen Abhängigkeiten in den Datenflüssen sind hierbei besonders entscheidend.

Ihre Qualifikation:

  • Studium der Informatik, Mathematik, Natur- oder Ingenieurwissenschaften
  • Programmiererfahrung (C++, Java, Python o.ä.)
  • Interesse an Verifikation und Validierung
  • Grundkenntnisse in formalen Sprachen und Aussagenlogik 
  • Interesse an Luftfahrt / Unbemannte Luftfahrzeuge
  • vorhandene Erfahrung mit SAT-/ SMT-Solvern

Ihr Start:

Freuen Sie sich auf einen Arbeitgeber, der Ihr Engagement zu schätzen weiß und Ihre Entwicklung durch vielfältige Qualifizierungs- und Weiterbildungsmöglichkeiten fördert.Unser einzigartiges Arbeitsumfeld bietet Ihnen Gestaltungsfreiräume und eine unvergleichbare Infrastruktur, in der Sie Ihre Mission verwirklichen können.Vereinbarkeit von Privatleben, Familie und Beruf sowie Chancengleichheit von Frauen und Männern sind wichtiger Bestandteil unserer Personalpolitik.Schwerbehinderte Bewerberinnen und Bewerber bevorzugen wir bei fachlicher Eignung.

39 weitere IT-Jobs von Deutsches Zentrum für Luft- und Raumfahrt (DLR)