Dissertation Oliver Keszöcze
Oliver Keszöcze hat seine Dissertation mit dem Titel "Exact Design of Digital Microfluidic Biochips" erfolgreich verteidigt. Der Fokus seiner Forschungsarbeit liegt auf der Optimierung des Designs von Digital Microfluidic Biochips (DMFB). Es handelt sich dabei um Geräte zur Miniaturisierung und Automatisierung von chemischen und biologischen Experimenten. In seiner Dissertation befasste sich Oliver Keszöcze mit dem Design-Problem für DMFBs. Hierbei geht es darum, ein gegebenes Experiment unter verschiedenen Constraints (Dauer, Größe des Biochips) auf einem Biochip zu realisieren. Insbesondere wurden die Teilprobleme "Routing" und "Pin Assignment" betrachtet. Die Zugehörigkeit zur Komplexitätsklasse NP konnte bewiesen werden, und es wurden Lösungen vorgestellt, welche Minimal-Lösungen erzeugen. Oliver Keszöcze entwickelte in seiner Dissertation einen Design-Ansatz, der alle einzelnen Teilprobleme - Binding, Scheduling, Placement, Routing und Pin Assignment - in einem Schritt löst, und somit Probleme beim Übergang zwischen den einzelnen Schritten vermeidet und insgesamt die beste Lösung erzeugt.
Wir gratulieren sehr herzlich und wünschen weiterhin viel Erfolg!

Dissertation Nils Przigoda
In seiner Dissertation beschäftigte sich Nils Przigoda mit der Validierung und Verifikation von UML/OCL Modellen mit formalen Methoden mit Hilfe von SMT-Beweisern. Hierzu wurde ein allgemeines Verfahren entwickelt, welches UML/OCL Modelle in ein für SMT-Beweiser gültiges Eingangsformat überführt. Dieser Vorgang wird auch als Modelltransformation oder kurz Transformation bezeichnet. Aufbauend hierauf wurden dann verschiedene Verfahren zur Validierung und Verifikation sowohl von strukturellen Eigenschaften als auch von Verhaltensaspekten von UML/OCL Modellen realisiert. Ein struktureller Ansatz ermittelt bei nicht-instanziierbaren Modellen (d.h. bei Modellen, die widersprüchliche Bedingungen enthalten) alle minimalen Gründe der Widersprüche. Ein anderer Aspekt der Arbeit beschäftigt sich mit der parallelen Ausführung von Methoden. Ferner wird in der Arbeit demonstriert, dass die entwickelten Ansätze auch in einem größeren Feld anwendbar sind. Exemplarisch wird dies anhand von Timing-Eigenschaften von MARTE/CCSL Modellen, einem UML2-Profil, demonstriert. Abschließend wird ein Ansatz zum Prüfen von einer gegebenen Implementierung einer Methode gegen die geforderten Eigenschaften auf der Modellebene vorgestellt. Insgesamt können mit den vorgestellten Ansätzen damit bereits vor einer Implementierung mannigfaltige Eigenschaften validiert und verifiziert sowie die Ergebnisse auf die nächsten Ebenen im Systementwurf übertragen werden. Ein Buchprojekt bei Springer ist in Planung.
Wir gratulieren sehr herzlich zur erfolgreichen Verteidigung!

Neu im Team
Seit 01.10. hat die Arbeitsgruppe Zuwachs bekommen: Wir freuen uns, dass Tim Meywerk nun zu unserem Team gehört und wünschen ihm einen guten Start in der AGRA! Im Rahmen des Sonderforschungsbereiches EASE beschäftigt er sich mit der formalen Verifikation und Verbesserung von Plänen für autonome Roboter. Darüber hinaus liegen seine Forschungsinteressen in den Gebieten des automatischen Schlussfolgerns und der Optimierung.

Damit das "Internet der Dinge" reibungslos funktioniert: Artikel in renommierterer Fachzeitschrift
Ob Sensoren in Kleidungsstücken oder medial vernetzte Haushalte: Das "Internet der Dinge" ("Internet of Things") gewinnt in unserem Alltag mehr und mehr an Bedeutung. Viele technische Fragen sind jedoch noch ungeklärt. Saeideh Shirinzadeh und Rolf Drechsler arbeiten mit internationalen Partnern daran, einzelne Speicher- und Datenprozesse in vernetzten Geräten und Gegenständen möglichst optimal und energiesparend zu steuern. Einen wichtigen Beitrag dafür haben wir jetzt gemeinsam mit Kollegen der École Polytechnique Fédérale de Lausanne (EPFL) in der Schweiz und der University of Utah, USA, in der renommierten IT-Fachzeitschrift IEEE Computer veröffentlicht.

In diesem Artikel stellen wir eine neu entwickelte Rechnerarchitektur vor. Sie soll die Voraussetzungen dafür schaffen, dass Computer in ihrem Speicher gleichzeitig Daten verarbeiten können - insbesondere im Anwendungsumfeld des "Internet of Things". Dieser Prozess verläuft bislang normalerweise getrennt; unsere neuen Erkenntnisse könnten die Basis dafür liefern, dass die Prozesse reibungsloser funktionieren und vernetzte Komponenten eine hohe Rechenleistung liefern, ohne unnötig viel Energie zu verbrauchen.

Den englischsprachigen Artikel mit dem Titel "A PLiM Computer for the Internet of Things" finden Sie hier.

Neues Springer-Buch "Formal System Verification"
Rolf Drechsler ist Herausgeber eines neuen Springer-Buches zur formalen Verifikation von Systemen. Das Buch vereint Beiträge aus Wissenschaft (seitens der Universitäten Freiburg, Frankfurt, Kaiserslautern und Oxford) und Industrie (OneSpin Solutions). Die Beiträge des Buches thematisieren den derzeitigen Stand der Forschung und zukünftige Trends im Bereich formaler Methoden. Dabei wird der gesamte Entwurfsablauf auf verschiedenen Abstraktionsebenen von ESL bis RTL betrachtet. Formale Verifikation wird sowohl in digitalen als auch in analogen Kontexten thematisiert, und es werden aktuelle Techniken aufgezeigt, die derzeit industriell eingesetzt werden.
Mehr Informationen gibt es hier.

Alumni-Stammbaum
Wir haben unsere akademischen Wurzeln über Günter Hotz (Gründungsmitglied und erster Vorsitzender der Gesellschaft für Informatik) und Leonhard Euler bis zu Gottfried Leibniz zurückverfolgt und sind stolz auf einen sehr beachtlichen Stammbaum! Wer wissen möchte, welche bedeutenden Wissenschaftler zu unseren "Ahnen" gehören, der findet sie hier.