Sie erforschen die Nutzung von formalen Methoden zur Qualitätssicherung von Ingenieurssoftware. Dazu nutzen Sie die verteilte Integrationsumgebung RCE (https://rcenvironment.de/) als konkreten Anwendungsfall. Die Desktop-Software RCE ermöglicht es Ingenieurinnen und Ingenieuren, Simulationen einzelner Aspekte komplexer Systeme wie Flugzeuge, Energie- oder Verkehrssysteme zu einer multidisziplinären Simulation zu kombinieren und in einer verteilten Rechenlandschaft auszuführen. Diese Rechnerlandschaft ist als Peer-to-Peer-Netzwerk realisiert. Alle Rechner befolgen dabei dasselbe Netzwerkprotokoll. Über dieses Protokoll werden Informationen über die Verfügbarkeit einzelner Rechner, verfügbare Einzelsimulationen oder den Ausführungsstatus von Gesamtsimulationen ausgetauscht.

Im Rahmen Ihrer Masterarbeit modellieren Sie dieses Netzwerkprotokoll in TLA+ und formulieren wünschenswerte Eigenschaften dieses Protokolls (wie z.B. Liveness, Deadlock-Freiheit oder Effektivität) als temporale Eigenschaften. Sie weisen entweder nach, dass das Protokoll diese wünschenswerten Eigenschaften erfüllt oder zeigen Ausführungswege auf, in denen diese Eigenschaften nicht erfüllt werden.

Sie arbeiten eigenständig an den genannten Aufgaben und stimmen sich dabei mit den anderen Teammitgliedern und der Gruppenleitung ab. Wir geben Ihnen die Freiheit und die Möglichkeit, eigene Ideen zu verfolgen und neue Forschungsthemen voranzutreiben. Wir bieten ein herausforderndes Arbeitsumfeld, bei dem Familienfreundlichkeit und Ihre Gesundheit oberste Priorität haben.