Tests können zwar in Software vorhandene Fehler aufdecken, die Abwesenheit von Fehlern kann man mittels Testen aber nicht beweisen. Hier setzt das Konzept der formalen Verifikation an. Schafft man es das Verhalten eines Systems in Form eines mathematischen Modells zu beschreiben, kann prinzipiell das Vorhandensein einer postulierten Korrektheitseigenschaft mathematisch, mittels Theorem-Proving oder Model-Checking,  bewiesen oder widerlegt werden. Der Einsatz dieser Methoden erscheint auf den ersten Blick als sehr vielversprechend, ihr Potential in der Praxis auszuschöpfen erweist sich jedoch als äusserst anspruchsvoll.

Treten Sie mit uns in Kontakt wenn Sie Fragen zu formalen Spezifikation- und Verifikationsmethoden haben.