Show simple item record

AuthorSchellhorn, Gerharddc.contributor.author
Date of accession2016-03-14T11:52:00Zdc.date.accessioned
Available in OPARU since2016-03-14T11:52:00Zdc.date.available
Year of creation1999dc.date.created
AbstractDie Arbeit stammt aus dem Themengebiet der Anwendung formaler Methoden im Software Engineering. Als Grundlage wurde die Spezifikationssprache der Abstrakten Zustandsmaschinen (engl. abstract state machines, kurz ASMs) verwendet. Inhalt der Arbeit ist die Entwicklung praktisch anwendbarer Werkzeugunterstützung für ASMs, sowohl für die Spezifikation, als auch für die Verifikation von Verfeinerungen. Diese macht die Entwicklung korrekter Software von einer abstrakten Anforderungsspezifikation bis hin zu einer durch schrittweise Verfeinerung gewonnenen Implementierung möglich. Der Inhalt gliedert sich in vier Teile: <br>- Definition einer 1:1-Einbettung von ASM-Spezifikationen in die Dynamische Logik (DL). Damit wird der formale Nachweis von ASM-Eigenschaften möglich. <br>- Modularisierung von Korrektheitsnachweisen für Verfeinerungen: Zwei Verfeinerungsbegriffe wurden in DL formalisiert. Ein allgemeines Modularisierungstheorem für den Korrektheitsnachweis von ASM-Verfeinerungen wurde entwickelt, das die bisher aus der Literatur bekannten Theoreme verallgemeinert. <br>- Implementierung der Ergebnisse im KIV-System, einem Spezifikations- und Verifikationswerkzeug für algebraische Spezifikationen und DL. <br>- Demonstration der praktischen Einsetzbarkeit der entwickelten Konzepte an einer großen Fallstudie aus dem Compilerbau: Diese behandelt die Übersetzung von Prolog-Programmen in Assemblercode der Warren Abstract Machine (WAM). Eine informelle Darstellung, die einen als ASM beschriebenen Prolog-Interpreter in 12 systematischen Verfeinerungen in die WAM transformiert, war vorgegeben. Die formale Spezifikation und Verifikation von 8 der 12 Verfeinerungen in 9 Monaten nahm eine großen Teil des Umfangs der Arbeit ein. Der Vergleich zu zwei anderen Fallstudien zum gleichen Thema zeigt, daß der notwendige Verifikationsaufwand durch die entwickelte Theorie für ASM-Verfeinerungen deutlich geringer war.dc.description.abstract
Languagededc.language.iso
PublisherUniversität Ulmdc.publisher
LicenseStandard (Fassung vom 03.05.2003)dc.rights
Link to license texthttps://oparu.uni-ulm.de/xmlui/license_v1dc.rights.uri
KeywordAbstract State Machinedc.subject
KeywordASMdc.subject
KeywordCompiler verificationdc.subject
KeywordDynamic logicdc.subject
KeywordDynamische Logikdc.subject
KeywordRefinementdc.subject
KeywordSpezifikationdc.subject
KeywordÜbersetzerverifikationdc.subject
KeywordVerfeinerungdc.subject
KeywordVerificationdc.subject
KeywordWAMdc.subject
KeywordWarren Abstract Machinedc.subject
Dewey Decimal GroupDDC 600 / Technology (Applied sciences)dc.subject.ddc
LCSHComputer programs. Verificationdc.subject.lcsh
LCSHComputer software. Specificationsdc.subject.lcsh
LCSHComputer systems. Specificationdc.subject.lcsh
TitleVerifikation abstrakter Zustandsmaschinendc.title
Resource typeDissertationdc.type
DOIhttp://dx.doi.org/10.18725/OPARU-6dc.identifier.doi
PPN1152300016dc.identifier.ppn
URNhttp://nbn-resolving.de/urn:nbn:de:bsz:289-vts-3468dc.identifier.urn
GNDAbstrakte Zustandsmaschinedc.subject.gnd
GNDPROLOG <Programmiersprache>dc.subject.gnd
GNDVerifikationdc.subject.gnd
FacultyFakultät für Informatikuulm.affiliationGeneral
Date of activation1999-12-10T10:57:19Zuulm.freischaltungVTS
Peer reviewneinuulm.peerReview
Shelfmark print versionO: J-H 5.435 ; W: W-H 6.250uulm.shelfmark
DCMI TypeTextuulm.typeDCMI
VTS-ID346uulm.vtsID
CategoryPublikationenuulm.category
University Bibliographyjauulm.unibibliographie


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record