Phased decomposition of distributed algorithms

Many distributed algorithms can be decomposed into subtasks, which are executed one after another from an abstract point of view, but are operationally concurrent. In this paper, we propose a proof method for this class of algorithms. We show, under which conditions it is possible, to infer the correctness of an algorithm from the correctness of its subtasks in isolation. We consider concurrent (i.e. partial order) runs of an algorithm and we explain the advantages of this kind of view for the described class of algorithms. We investigate a minimum spanning tree algorithm to illustrate the method. The results are formalized in the Distributed Algorithms Working Notation (DAWN), where a distributed algorithm is modeled by a high-level Petri netAvailable from TIB Hannover: RR 2036(120) / FIZ - Fachinformationszzentrum Karlsruhe / TIB - Technische InformationsbibliothekSIGLEDEGerman