WikiDer > Formale Methoden

Formele methoden

EIN formale Methode ist eine op Mathematik und formale Logik basierte Methode zu Software und Hardwaresysteme zu spezifizieren und zu überprüfen. Der Zweck (der Einsatz von) formalen Methoden ist:

  • es eindeutig und völlig den Betrieb eines zu entwerfenden Programms spezifizieren oder Algorithmus, und
  • systematischer und schlüssiger Nachweis der Korrektheit eines Programms oder Algorithmus.

Spezifikation

Mit formalen Methoden kann die Funktionsweise eines zu entwerfenden Systems oder Algorithmus durch mathematische und logische Notationen beschrieben werden. Diese sind im Gegensatz zu Beschreibungen in gesprochener Sprache eindeutig und methodisch überprüfbar. Ein Beispiel dafür ist BNF, die es ermöglicht, die Syntax einer Sprache (die Grammatik) eindeutig zu notieren.

Überprüfung

Die formale Spezifikation kann dann verwendet werden, um die Korrektheit der Spezifikation zu beweisen. Dies zeigt im Erfolgsfall auch die Korrektheit der Umsetzung, wenn sie tatsächlich den aufgestellten Spezifikationen entspricht.

Aufgrund der Natur formaler Methoden ist es (zum Teil) möglich, diesen Prozess zu automatisieren.

Formale Methoden und Notationen

Es stehen eine Reihe von formalen Methoden und Notationen zur Verfügung, wie zum Beispiel: