Benutzer: Gast  Login
Titel:

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

Dokumenttyp:
Technical Report
Autor(en):
Johann Schumann; Max Breitling
Abstract:
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,...     »
Stichworte:
Verifikation; Verfeinerung; Theorembeweiser; Focus; AutoFocus; Setheo; SMV; zweielementiger Puffer
Jahr:
1999
Jahr / Monat:
1999-01-01 00:00:00
Seiten/Umfang:
33
 BibTeX