Suche

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.