Paper Info
Title
Integrating distibuted algorithms into distributed systems
Abstract
A distributed algorithm is often used as a part of a larger distributed system. Usually, the properties of an algorithm are proven for the algorithm in isolation. Then, it is not obvious how the algorithm behaves when integrated into a larger system. In this paper, we present a simple technique which allows to derive properties of an algorithm which is integrated into a distributed system from the properties of the algorithm in isolation. The technique exploits the fact that some actions of a distributed algorithm do not belong to the algorithm but are triggered by the environment. If these actions are distinguished and are adequately considered in the verification of the algorithm, basically all properties are still valid for the algorithm as a part of a larger distributed system. This result will be formalized in the setting of the Distributed Algorithms' Working Notation (DAWN). Based on this result, we will give a proof rule which allows to prove liveness properties of a system from liveness properties of the involved distributed algorithm.
Year
DOI
Venue
1999
10.3233/FI-1999-37306
Fundam. Inform.
Keywords
Field
DocType
proof rule,distibuted algorithm,working notation,liveness property,simple technique,larger system,temporal logic,compositionality,distributed algorithms,petri net,distributed algorithm,distributed system
Principle of compositionality,Notation,Petri net,Distributed minimum spanning tree,Parallel algorithm,Computer science,Algorithm,Theoretical computer science,Distributed algorithm,Temporal logic,Liveness,Distributed computing
Journal
Volume
Issue
Citations 
37
3
2
PageRank 
References 
Authors
0.39
8
2
Name
Order
Citations
PageRank
Ekkart Kindler11219105.52
Sibylle Peuker292.65