Formalisierung und Beweis einer Verfeinerung aus FOCUS mit automatischen Theorembeweisern - Fallstudie -

Das Ziel dieser Arbeit ist eine Evaluierung inwieweit der Theorembeweiser SETHEO an das Spezifikationswerkzeug AUTOFOCUS zur weitgehend automatischen Durchfuehrung von Verifikationsaufgaben angeschlossen werden kann. Dazu wurde ein zweielementiger Puffer sowohl abstrakt durch eine einzelne Komponente spezifiziert, als auch als verteiltes System, bestehend aus zwei einelementigen Puffern und einer Kontrolleinheit. Aus den graphisch erstellten Spezifikationen wurden formale Darstellungen erzeugt, mit denen der Beweis der Verfeinerungsrelation zwischen den beiden Spezifikationen mit Hilfe der automatischen Beweiser SETHEO und SMV durchgefuehrt werden konnte.     «

Das Ziel dieser Arbeit ist eine Evaluierung inwieweit der Theorembeweiser SETHEO an das Spezifikationswerkzeug AUTOFOCUS zur weitgehend automatischen Durchfuehrung von Verifikationsaufgaben angeschlossen werden kann. Dazu wurde ein zweielementiger Puffer sowohl abstrakt durch eine einzelne Komponente spezifiziert, als auch als verteiltes System, bestehend aus zwei einelementigen Puffern und einer Kontrolleinheit. Aus den graphisch erstellten Spezifikationen wurden formale Darstellungen erzeugt,...     »