• English
    • Deutsch
  • English 
    • English
    • Deutsch
  • Login
View Item 
  •   Home
  • Universität Ulm
  • Publikationen
  • View Item
  •   Home
  • Universität Ulm
  • Publikationen
  • View Item
JavaScript is disabled for your browser. Some features of this site may not work without it.

Verifikation abstrakter Zustandsmaschinen

Thumbnail
vts_346.pdf (1.172Mb)
211 Seiten
Veröffentlichung
1999-12-10
Authors
Schellhorn, Gerhard
Dissertation


Faculties
Fakultät für Informatik
Abstract
Die 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.
Date created
1999
Subject headings
[GND]: Abstrakte Zustandsmaschine | PROLOG <Programmiersprache> | Verifikation
[LCSH]: Computer programs. Verification | Computer software. Specifications | Computer systems. Specification
[Free subject headings]: Abstract State Machine | ASM | Compiler verification | Dynamic logic | Dynamische Logik | Refinement | Spezifikation | Übersetzerverifikation | Verfeinerung | Verification | WAM | Warren Abstract Machine
[DDC subject group]: DDC 600 / Technology (Applied sciences)
License
Standard (Fassung vom 03.05.2003)
https://oparu.uni-ulm.de/xmlui/license_v1

Metadata
Show full item record

DOI & citation

Please use this identifier to cite or link to this item: http://dx.doi.org/10.18725/OPARU-6

Schellhorn, Gerhard (1999): Verifikation abstrakter Zustandsmaschinen. Open Access Repositorium der Universität Ulm und Technischen Hochschule Ulm. Dissertation. http://dx.doi.org/10.18725/OPARU-6
Citation formatter >



Policy | kiz service OPARU | Contact Us
Impressum | Privacy statement
 

 

Advanced Search

Browse

All of OPARUCommunities & CollectionsPersonsInstitutionsPublication typesUlm SerialsDewey Decimal ClassesEU projects UlmDFG projects UlmOther projects Ulm

My Account

LoginRegister

Statistics

View Usage Statistics

Policy | kiz service OPARU | Contact Us
Impressum | Privacy statement