Studien-/ Abschlussarbeit, Praktikum Generierung von Inputsequenzen zum Test und zur Analyse von Monitor-Spezifikationen Student/in Informatik, Mathematik, Naturwissenschaften o.ä.

Starten Sie Ihre Mission beim DLR.

Das DLR ist das Forschungszentrum für Luft- und Raumfahrt sowie die Raumfahrtagentur der Bundesrepublik Deutschland. Rund 8.000 Mitarbeiterinnen und Mitarbeiter forschen gemeinsam an einer einzigartigen Vielfalt von Themen in Luftfahrt, Raumfahrt, Energie, Verkehr, Digitalisierung und Sicherheit. Ihre Missionen reichen von der Grundlagenforschung bis hin zur Entwicklung von innovativen Anwendungen und Produkten von morgen. Spitzenforschung braucht auf allen Ebenen exzellente Köpfe – insbesondere noch mehr weibliche – die Ihre Potenziale in einem inspirierenden Umfeld voll entfalten. Starten Sie Ihre Mission bei uns.

Für unser Institut Flugsystemtechnik in Braunschweig suchen wir eine/n

Generierung von Inputsequenzen zum Test und zur Analyse von Monitor-Spezifikationen

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.

Fachliche Fragen beantwortet Ihnen gern Sebastian Schirmer telefonisch unter +49 531 295-2858. Weitere Informationen zu dieser Position mit der Kennziffer 23044 sowie zum Bewerbungsweg finden Sie unter www.DLR.de/dlr/jobs/#28512.