Wir trauern um unseren Freund und Kollegen Daniel Wonisch.

21.2.2012

Fachgebiet Spezifikation und Modellierung von Softwaresystemen

Willkommen beim Webangebot der Fachgruppe "Spezifikation und Modellierung von Softwaresystemen"! Das Arbeitsgebiet der Fachgruppe ist die modellbasierte Softwareentwicklung mit formalen Methoden. Als formale Methoden bezeichnet man Sprachen zur Beschreibung (Spezifikation) von Software und Hardware, die eine formale, mathematisch exakt beschriebene Semantik besitzen. Ziel einer solchen Entwicklungsmethodik ist der Entwurf hochgradig zuverlässiger, korrekter Systeme. 

Die Arbeiten der Fachgruppe lassen sich aus der Sicht der Grundlagenforschung dabei in drei Bereiche teilen: die Entwicklung von Semantiken für Modellierungsformalismen, die Erforschung von Verifikationstechniken zum Nachweis von Korrektheit und die Definition von Verfeinerungsbegriffen für Modelltransformationen. Auf der Anwendungsseite beschäftigen wir uns mit dem Einsatz dieser Methoden in service-orientierten Architekturen, in mechatronischen Systemen (speziell für Rekonfiguration) und für lockfreie Algorithmen. 

Momentan beschäftigen wir uns in den drei Bereichen mit folgenden Arbeiten: 

• Sprachen und Semantik:
  • Refactoringssprachen und Korrektheit von Refactorings

• Verifikation:
  • Kompositionelle Verifikation und Dekomposition von Modellen
  • Abstraktionstechniken für parallele Systeme (DFG Projekt ViPar)
  • Shape-Analysen für Graphstranformationssysteme (SFB 614, Teilprojekt B1)
  • Kompositionsanalyse in unsicheren Kontexten (SFB 901, Teilprojekt B3)
  • Proof-Carrying Code (SFB 901, Teilprojekt B4)
  • Desweiteren besteht im Bereich Verifikation eine Kooperation mit dem Teilprojekt R1 des SFB/TR 14 AVACS. 

• Verfeinerung:
  • Korrektheit von Modelltransformationen (Kooperation mit U. Twente und U. Duisburg-Essen)
  • Linearisierbarkeit lockfreier Algorithmen (Kooperation mit U. Augsburg und U. Sheffield)