Benutzer: Gast  Login
Dokumenttyp:
Technical Report 
Autor(en):
Johann Schumann; Max Breitling 
Titel:
Formalisierung und Beweis einer Verfeinerung aus FOCUS mit automatischen Theorembeweisern - Fallstudie - 
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