OS-Updates

Heute größere OS-Update-Runde. Downtime von 16:00 bis 17:00.

Diplomthema zu vergeben

Thema: Verifikation der Lebendigkeit von Rekonfigurationen in Qualitäts-behafteten,  Selbst-optimierenden Systemen

Zielstellung:

Im Rahmen des SFB 912 und der ESF-geförderten Nachwuchsforschergruppe ZESSY wird ein selbst-adaptives System entwickelt, welches sein Verhalten hinsichtlich nicht-funktionaler Eigenschaften (Qualitäten) selbstständig optimiert. Hierzu wurde eine Komponenten-basierte Softwarearchitektur entwickelt, die die Beschreibung von Software- und Hardware-Komponenten und deren Abhängigkeiten untereinander erlaubt. Die Abhängigkeiten werden über Verträge zwischen den Komponenten beschrieben, in denen Spielräume zur Verhandlung von Qualitäten definiert werden. Den Benutzern eines solchen Systems wird es somit ermöglicht, Erwartungen an die Ausführung der Funktionalität des Systems zu stellen (zum Beispiel eine minimale Bildrate  bei der Wiedergabe eines Videos). Mit Hilfe von Optimierungstechniken kann für eine solche Anfrage eine optimale Systemkonfiguration, bestehend aus der Auswahl geeigneter Implementierungen von Softwarekomponenten und deren Mapping auf die verfügbaren Ressourcen, gefunden werden. Um von der aktuellen Systemkonfiguration zur optimalen Konfiguration zu gelangen werden Rekonfigurationsskripte, welche eine Folge von Rekonfigurationsoperationen (deploy, undeploy, migrate, replace, etc.) beschreiben, abgeleitet.

Ziel der Diplomarbeit ist die Anwendung von Verifikationstechniken aus dem Bereich des Model Checking um Rekonfigurationsskripte auf deren Lebendigkeit zu untersuchen. Hierzu soll Vereofy und dessen Koordinationssprache Reo verwendet werden. Wenn ein Skript das System zeitweise in einen inkonsistenten Zustand überführen kann, soll dies erkannt und aufgezeigt werden.

Im Detail sind folgende Teilaufgaben zu bearbeiten:

• Einarbeitung in die Softwarearchitektur für selbst-optimierende Systeme (CCM/QCL)
• Einarbeitung in Vereofy, insbesondere die Koordinationssprache Reo
• Implementierung der Übersetzung von CCM/QCL-Modellen und der Rekonfigurationsskripte in Reo
• Formulierung der Lifeness-Anforderung
• Integration in die qBench IDE (Eclipse)

Die Arbeit wird vom Lehrstuhl für Softwaretechnologie und dem Lehrstuhl für algebraische und logische Grundlagen der Informatik co-betreut.