Zur Kurzanzeige

2001-07-03Dissertation DOI: 10.18452/14640
Halbordnungsbasierte Verfeinerung zur Verifikation verteilter Algorithmen
dc.contributor.authorPeuker, Sibylle
dc.date.accessioned2017-06-18T04:28:00Z
dc.date.available2017-06-18T04:28:00Z
dc.date.created2001-07-03
dc.date.issued2001-07-03
dc.identifier.urihttp://edoc.hu-berlin.de/18452/15292
dc.description.abstractIn 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.ger
dc.description.abstractThe 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.eng
dc.language.isoger
dc.publisherHumboldt-Universität zu Berlin, Mathematisch-Naturwissenschaftliche Fakultät II
dc.rights.urihttp://rightsstatements.org/vocab/InC/1.0/
dc.subjectVerifikationger
dc.subjectVerfeinerungger
dc.subjectNebenläufigkeitger
dc.subjectPetrinetzeger
dc.subjectverteilte Algorithmenger
dc.subjectHalbordnungssemantikger
dc.subjectdistributed algorithmseng
dc.subjectverificationeng
dc.subjectrefinementeng
dc.subjectconcurrencyeng
dc.subjectPetri netseng
dc.subjectpartial order semanticseng
dc.subject.ddc004 Informatik
dc.titleHalbordnungsbasierte Verfeinerung zur Verifikation verteilter Algorithmen
dc.typedoctoralThesis
dc.identifier.urnurn:nbn:de:kobv:11-10015558
dc.identifier.doihttp://dx.doi.org/10.18452/14640
dc.date.accepted2001-07-03
dc.contributor.refereeStarke, Peter
dc.contributor.refereeRoever, Willem-Paul de
dc.contributor.refereeReisig, Wolfgang
dc.subject.dnb28 Informatik, Datenverarbeitung
dc.subject.rvkST 130
local.edoc.pages170
local.edoc.type-nameDissertation
bua.departmentMathematisch-Naturwissenschaftliche Fakultät II

Zur Kurzanzeige