Technical Report
Formalisierung und Beweis einer Verfeinerung aus FOCUS mit automatischen Theorembeweisern - Fallstudie -
Author(s): Johann Schumann, Max Breitling
Year: 1999
Number: TUM-I9904
Editor:
CR Classification: D.2.1, D.2.4, F.3.1
CR General Terms: Verification
Keywords: Verifikation, Verfeinerung, Theorembeweiser, Focus, AutoFocus, Setheo, SMV, zweielementiger Puffer
Version
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, mit denen der Beweis der
Verfeinerungsrelation zwischen den beiden Spezifikationen mit Hilfe der
automatischen Beweiser SETHEO und SMV durchgefuehrt werden konnte.
Available as compressed Postscript
BibTeX-Entry:
<![CDATA[
@techreport{SB99,
author = {Johann Schumann and Max Breitling},
title = {Formalisierung und Beweis einer Verfeinerung aus FOCUS mit automatischen Theorembeweisern - Fallstudie -},
number = {TUM-I9904},
institution = {Technische Univerit\"at M\"unchen},
year = {1999},
url = {http://www4.informatik.tu-muenchen.de/reports/SB99.html},
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, mit denen der Beweis der
Verfeinerungsrelation zwischen den beiden Spezifikationen mit Hilfe der
automatischen Beweiser SETHEO und SMV durchgefuehrt werden konnte.},
CRClassification = {D.2.1, D.2.4, F.3.1},
CRGenTerms = {Verification}}
]]>