Integrating Distributed Algorithms into Distributed Systems

Distributed algorithms are often part of a larger distributed system. Usually the properties of the algorithm are proven for the algorithm in isolation. Then, it is not obvious how the algorithm behaves integrated into a larger system. In this paper we exploit the simple observation 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 adequately considered in the veri cation 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)