edoc-Server der Humboldt-Universität zu Berlin

Dissertation

Autor(en): Sibylle Peuker
Titel: Halbordnungsbasierte Verfeinerung zur Verifikation verteilter Algorithmen
Gutachter: Peter Starke; Willem-Paul de Roever; Wolfgang Reisig
Erscheinungsdatum: 03.07.2001
Volltext: pdf (urn:nbn:de:kobv:11-10015558)
Fachgebiet(e): Informatik
Schlagwörter (ger): Verifikation, Verfeinerung, Nebenläufigkeit, Petrinetze, verteilte Algorithmen, Halbordnungssemantik
Schlagwörter (eng): distributed algorithms, verification, refinement, concurrency, Petri nets, partial order semantics
Einrichtung: Humboldt-Universität zu Berlin, Mathematisch-Naturwissenschaftliche Fakultät II
Zitationshinweis: Peuker, Sibylle: Halbordnungsbasierte Verfeinerung zur Verifikation verteilter Algorithmen; Dissertation, Humboldt-Universität zu Berlin, Mathematisch-Naturwissenschaftliche Fakultät II , publiziert am 03.07.2001, urn:nbn:de:kobv:11-10015558
Metadatenexport: Um den gesamten Metadatensatz im Endnote- oder Bibtex-Format zu speichern, klicken Sie bitte auf den entsprechenden Link. Endnote   Bibtex  
print on demand: Wenn Sie auf dieses Icon klicken, können Sie ein Druckexemplar dieser Publikation bestellen.
Diese Seite taggen: Diese Icons führen auf so genannte Social-Bookmark-Systeme, auf denen Sie Lesezeichen anlegen, persönliche Tags vergeben und Lesezeichen anderer Nutzer ansehen können.
  • connotea
  • del.icio.us
  • Furl
  • RawSugar

Abstract (ger):
In dieser Arbeit geht es um die schrittweise Verfeinerung verteilter Algorithmen. Dabei wird ein einfacher Algorithmus, der einige gewünschte Eigenschaften hat, Schritt für Schritt zu einem komplexen Algorithmus verfeinert, der konkrete Implementationsanforderungen erfüllt, so daß in jedem Schritt die gewünschten Eigenschaften erhalten bleiben. Wir stellen einen neuen eigenschaftserhaltenden Verfeinerungsbegriff vor, der auf der kausalen Ordnung der Aktionen eines Algorithmus basiert. Diesen Begriff definieren wir als Transitionsverfeinerung für elementare Petrinetze und diskutieren Beweiskriterien. Danach definieren und diskutieren wir die simultane Verfeinerung mehrerer Transitionen. Zur Modellierung komplexer verteilter Algorithmen sind elementare Petrinetze oft nicht adäquat. Wir benutzen deshalb algebraische Petrinetze. Wir definieren Transitionsverfeinerung für algebraische Petrinetze und stellen einen Zusammenhang zur simultanen Verfeinerung von Transitionen in elementaren Petrinetzen her. Transitionsverfeinerung ist besonders für Verfeinerungsschritte geeignet, in denen synchrone Kommunikation zwischen Agenten durch asynchronen Nachrichtenaustausch ersetzt wird. Wir zeigen dies am Beispiel eines komplexen verteilten Algorithmus, zur Berechnung des minimalen spannenden Baumes in einem gewichteten Graphen. Wir zeigen die Korrektheit dieses Algorithmus in mehreren Schritten, von denen einige Schritte Transitionsverfeinerungen sind. In anderen Schritten sind klassische Verfeinerungsbegriffe ausreichend. Wir übertragen deshalb auch einen klassischen Verfeinerungsbegriff in unser formales Modell.
Abstract (eng):
The topic of this PhD thesis is the stepwise refinement of distributed algorithms. Stepwise refinement starts with a simple algorithm with certain desired properties. This algorithm is refined step by step such that the desired properties are preserved in each refinement step. The result is a complex distributed algorithm which satisfies concrete implementation requirements and which still has the desired properties. We propose a new property preserving notion of refinement which is based on the causal ordering of actions of an algorithm. We call this notion transition refinement and we define it first for elementary Petri nets. Furthermore, we discuss proof criteria. Then, we define and discuss the simultaneous refinement of several transitions. For modelling complex distributed algorithms, we use algebraic Petri nets instead of elementary Petri nets. We define transition refinement for algebraic Petri nets, and we show its relationship to simultaneous transition refinement in elementary Petri nets. Transition refinement is particularly suitable for refinement steps in which synchronous communication between agents is replaced by asynchronous message passing. We show this by means of a complex distributed algorithm for determining the minimal spanning tree of a weighted graph. We prove the correctness of this algorithm in several steps. Some of these steps are transition refinements. For other steps, well-known notions of refinement are sufficient. Therefore, we also carry over a well-known notion of refinement into our formal model.
Zugriffsstatistik: Die Daten für die Zugriffsstatistik der einzelnen Dokumente wurden aus den durch AWStats aggregierten Webserver-Logs erstellt. Sie beziehen sich auf den monatlichen Zugriff auf den Volltext sowie auf die Startseite. Die Zugriffsstatistik wird nicht standardisiert erfasst und kann maschinelle Zugriffe enthalten.
 
Bei Formatversionen eines Dokuments, die aus mehreren Dateien bestehen (insbesondere HTML), wird jeweils der monatlich höchste Zugriffswert auf eine der Dateien (Kapitel) des Dokuments angezeigt.
 
Um die detaillierten Zugriffszahlen zu sehen, fahren Sie bitte mit dem Mauszeiger über die einzelnen Balken des Diagramms.
Startseite: 2 Zugriffe PDF: 3 Zugriffe PDF: 4 Zugriffe Startseite: 4 Zugriffe PDF: 3 Zugriffe Startseite: 2 Zugriffe PDF: 4 Zugriffe Startseite: 2 Zugriffe PDF: 7 Zugriffe PDF: 7 Zugriffe PDF: 8 Zugriffe PDF: 15 Zugriffe PDF: 7 Zugriffe Startseite: 4 Zugriffe PDF: 16 Zugriffe Startseite: 4 Zugriffe PDF: 9 Zugriffe Startseite: 4 Zugriffe PDF: 13 Zugriffe PDF: 8 Zugriffe PDF: 7 Zugriffe PDF: 16 Zugriffe PDF: 8 Zugriffe Startseite: 3 Zugriffe PDF: 18 Zugriffe Startseite: 2 Zugriffe PDF: 33 Zugriffe PDF: 11 Zugriffe Startseite: 1 Zugriffe PDF: 15 Zugriffe PDF: 20 Zugriffe PDF: 10 Zugriffe Startseite: 3 Zugriffe PDF: 13 Zugriffe Startseite: 3 Zugriffe PDF: 21 Zugriffe PDF: 14 Zugriffe Startseite: 3 Zugriffe PDF: 11 Zugriffe Startseite: 2 Zugriffe PDF: 36 Zugriffe Startseite: 2 Zugriffe PDF: 25 Zugriffe PDF: 17 Zugriffe Startseite: 2 Zugriffe PDF: 26 Zugriffe PDF: 13 Zugriffe Startseite: 2 Zugriffe PDF: 19 Zugriffe Startseite: 5 Zugriffe PDF: 24 Zugriffe PDF: 17 Zugriffe Startseite: 1 Zugriffe PDF: 29 Zugriffe Startseite: 2 Zugriffe PDF: 14 Zugriffe Startseite: 1 Zugriffe PDF: 12 Zugriffe
Jul
11
Aug
11
Sep
11
Oct
11
Nov
11
Dec
11
Feb
12
Apr
12
May
12
Jun
12
Jul
12
Aug
12
Sep
12
Oct
12
Nov
12
Dec
12
Jan
13
Feb
13
Mar
13
Apr
13
May
13
Jun
13
Jul
13
Aug
13
Sep
13
Oct
13
Nov
13
Dec
13
Jan
14
Feb
14
Mar
14
Apr
14
May
14
Jun
14
Jul
14
Aug
14
Sep
14
Monat Jul
11
Aug
11
Sep
11
Oct
11
Nov
11
Dec
11
Feb
12
Apr
12
May
12
Jun
12
Jul
12
Aug
12
Sep
12
Oct
12
Nov
12
Dec
12
Jan
13
Feb
13
Mar
13
Apr
13
May
13
Jun
13
Jul
13
Aug
13
Sep
13
Oct
13
Nov
13
Dec
13
Jan
14
Feb
14
Mar
14
Apr
14
May
14
Jun
14
Jul
14
Aug
14
Sep
14
Startseite 2   4 2 2         4 4 4         3 2   1     3 3   3 2 2   2   2 5   1 2 1
PDF 3 4 3 4 7 7 8 15 7 16 9 13 8 7 16 8 18 33 11 15 20 10 13 21 14 11 36 25 17 26 13 19 24 17 29 14 12

Gesamtzahl der Zugriffe seit Jul 2011:

  • Startseite – 54 (1.46 pro Monat)
  • PDF – 533 (14.41 pro Monat)
 
 
Generiert am 25.10.2014, 13:58:26