Algebraische Systembeschreibung
Formale Methoden dienen der Erstellung nachweisbar korrekter Systeme, sowohl in Soft- wie in Hardware. Hierzu gibt es zwei wesentliche Ans?tze:
- Umformung einer (h?ufig noch nicht ausführbaren) formalen Spezifikation durch Semantik-treue Transformationen in eine per Konstruktion korrekte Implementierung (Transformations-/Verfeinerungsansansatz)
- Angabe von Spezifikation und Implementierung mit anschlie?endem Beweis der Korrektheit der Implementierung relativ zur Spezifikation (Verifikationsansatz).
Beide dieser Ans?tze, insbesondere aber der Transformationsansatz, k?nnen für auch nur halbwegs realistische Systeme nur dann in voller Formalit?t durchgeführt werden, wenn in gro?em Umfang algebraische Techniken eingesetzt werden, die viele kleine logische Umformungsschritte durch Anwendung eines einzigen gro?en (Un-)gleichungsschritts ersetzen. Hierzu sind geeignete algebraische Strukturen und Modellierungsm?glichkeiten zu finden.
Grundlegende Strukturen
Als grundlegende algebraische Strukturen zur Systembeschreibung haben sich unter anderem Halbringe, Kleene-Algebren und Omega-Algebren erwiesen. Die gegenw?rtigen Forschungsarbeiten der Professur besch?ftigen sich mit der Weiterentwicklung und Anpassung dieser Strukturen in konkreten Anwendungsf?llen.
?
?
Semantik
Unabdingbare Grundlage für die formale Systembeschreibung und -entwicklung ist eine formal definierte Semantik für die Konstrukte der verwendeten Spezifikations- und Implementierungssprachen. Um einen nahtlosen ?bergang zu erm?glichen, werden auch hier algebraische Techniken zur Semantikdefinition eingesetzt, so dass die zugeh?rigen Gesetze direkt für die Systementwicklung nutzbar werden.
?