Forschung
Ausrichtung: Die Hauptvision unserer Forschung ist es, praxistaugliche Modellierungs- und Analysetechniken zur Entwicklung und Wartung von hochwertiger Softwaresysteme zu entwerfen und zu implementieren. Durch eine enge Einbindung von flexibel transformierbaren und inkrementell verifizierbaren Modellen in den Entwicklungsprozess, können wir die steigende Komplexität sowie Heterogenität von heutigen daten- und softwareintensiven Systemen und die erhöhten Anforderungen an deren Anpassbarkeit mit einem klaren Bekenntnis zu Qualität bewältigen. Unser Ansatz zur Konstruktion und Qualitätssicherung von Softwaresystemen basiert deshalb auf der Integration der folgenden Forschungsfelder:
- Model Engineering: zur Konstruktion von Modellen für Systeme
- Transformation Engineering: zur Konstruktion von automatischen (deterministischen sowie suchbasierten & randomisierten) Methoden zur Transformation von Systemen
- Verification Engineering: zur Konstruktion von Techniken (Analyse, Test, formale Verifikation), die eine Qualitätssicherung im gesamten Lebenszyklus von Systemen unterstützen.
Grundlagen: Da die unterliegende Struktur von Modellen durch Graphen beschrieben werden kann, ist Graphtransformation ein geeignetes Mittel, um Modelltransformationen zu spezifizieren. Daneben bietet sich Graphtransformation auch zur Verwaltung und Evolution von semi-strukturierten Daten an. Wir verwenden deshalb Graph- und Graphtransformationstheorie als solide Wegbereiter für das Zusammenspiel der oben genannten Forschungsfelder. In diesem Fokus erarbeiten wir die folgenden Grundlagen:
- Logik und Graphen: automatisches Beweisen und SAT Solving von Grapheigenschaften, automatische Reparatur von Graphen
- Graphtransformation: Analyse, Test, formale Verifikation
- Kategorientheorie für Transformationssysteme: Konsolidierung und Vereinheitlichung der Transformationstheorie für unterschiedliche Varianten von höheren Strukturen wie getypte Graphen, Graphen mit Labels, Tripel-Graphen, Hypergraphen, Petrinetze, attributierte Graphen, algebraische Spezifikationen, etc.
QS-Techniken: Basierend auf diesen Grundlagen streben wir fortlaufend die Entwicklung und Implementierung von QS-Techniken an, die sowohl grundlegende Ingenieursprinzipien wie Ausdrucksmächtigkeit, Effizienz, und Benutzbarkeit berücksichtigen als auch allgemeingültig sind. Das Gesamtziel ist es dabei, QS-Techniken zu erstellen, die eng mit dem Softwareentwicklungsprozess verschränkt sind und einen angemessenen Grad an Automatisierung sowie menschlicher Interaktion beinhalten. Ausgewählte Beispiele von QS-Techniken, die wir erforschen, sind die folgenden:
- Konflikt- und Abhängigkeitserkennung in Anforderungsspezifikationen
- Plausibilitätsprüfung von ausführbaren Modellen
- Verifikation der Konsistenz- und Verhaltensbewahrung, bzw. des funktionalen Verhaltens von Modelltransformationen (insbesondere Modell-Refactorings)
- Testen der Konformität von Tripel-Graphgrammatik Implementierungen
- Modellbasiertes Testen von Graphdatenbanken und Graphdatenbankanwendungen.
Aktuelle und zukünftige Beispielherausforderungen und -anwendungsdomänen fokussieren sich vorrangig auf die fortgeschrittene Automatisierung der Konstruktion und Qualitätssicherung von daten- und softwareintensiven Systemen. Die Medizininformatik wollen wir dabei als einen der wichtigsten Vertreter auf diesem Gebiet fokussieren.