TFS - Profil

Im Fachgebiet TFS werden formale Techniken zur Spezifikation von Systemen untersucht. Hierbei werden sowohl die Spezifikationen selbst (die Syntax), als auch ihre Bedeutung (die Semantik) mit mathematischen Formalismen beschrieben. Dies ermöglicht die präzise Behandlung von Phänomenen wie Korrektheit, Komposition, Verfeinerung und Übersetzung von Spezifikationen. Die dabei entstehenden, fundierten Modellierungs- und Spezifikations-techniken finden ihre Anwendung in der Softwaretechnik, wobei der Einsatz von formalen Techniken dazu führt, dass schon während Anforderungsanalyse und Entwurf eines Systems detaillierte Aussagen über seine späteren Eigenschaften möglich sind. Die in Syntax und Semantik auftauchenden Strukturen kommen aus unterschiedlichen Bereichen der Mathematik. So eignen sich algebraische Strukturen mit Mengen und Abbildungen für die Modellierung von Datenstrukturen, während graphische Strukturen mit Knoten und Kanten für die Darstellung von visuellen Sprachen geeignet sind. Als eine gemeinsame Grundlage dieser vielfältigen mathematischen Objekte wird die Kategorientheorie verwendet.

Ein besonderer Schwerpunkt sind die visuellen Sprachen, in welchen Systeme nicht durch Texte, sondern durch Diagramme beschrieben werden. Diese gewinnen in der Informatik immer mehr an Bedeutung, da sie die Kommunikation der Entwickler untereinander und mit den Anwendern erleichtern. Wichtige aktuelle Forschungsgebiete sind hier Modelltransformationen, welche zur Übersetzung zwischen verschiedenen visuellen Sprachen eingesetzt werden können, und so genannte „Domain Specific Languages“, welche eine an ein bestimmtes Anwendungsgebiet angepasste Modellierung ermöglichen. Im Bereich visueller Sprachen fließen die theoretischen Ergebnisse direkt in selbst entwickelte Werkzeuge ein, z.B. in den Designer und Generator für Editoren visueller Sprachen (TIGER) sowie in die Entwicklungs- und Anwendungsumgebung für attributierte Graphgrammatiken (AGG) und das Modellierungswerkzeug für Rekonfigurierbare Objektnetze (RON).

Aktuelle Forschungsrichtungen sind:

Formale Spezifikationstechniken

• Algebraische Spezifikation von Datentypen
• Petrinetze zur Spezifikation von Prozessen
• Graphtransformation und Visuelle Modellierung

Allgemeine Konzepte für Spezifikationstechniken

• Parametrisierung und Modularisierung, Komponentenkonzepte
• Korrektheit, Verfeinerung und Refactoring von Spezifikationen
• Formaler Entwurf, Analyse und Korrektheit von Modelltransformationen
• Integration von heterogenen Spezifikations- und Modellierungstechniken
• Einbettung in den Softwareentwicklungsprozess
• Modellgesteuerte Softwareentwicklung
• Modellierung mit UML (Unified Modeling Language)
• Formale Methoden in Anforderungs- und Entwurfsspezifikationen
• Prototypische Implementierung theoretischer Ergebnisse

Lehre:

Neben der Beteiligung am TheGI-Zyklus in der Grundausbildung Informatik stellen wir weiterführende Angebote zur Verfügung. Dabei werden die Themen Graph- und Modelltransformation, Spezifikation mit Graphtransformation, Petrinetzen und Komponentenkonzepten sowie deren Fundamente im Bereich Algebraischer Spezifikation und Kategorientheorie behandelt. Bekannte Techniken mit ähnlicher Ausrichtung, z.B. die Metamodellierung, werden detailliert in Beziehung gesetzt.