Volume 8 : Number 1 : Paper 2
August 2005 Special Issue of Best Papers presented at CLEI2004, Arequipa, Peru
Title:
Facilitating the Verification of Diffusing Computations and Their Applications

Authors and Affiliations:
S. Doaitse S. Swierstra,
Tanja E.J. Vos,

Abstract:
We study a class of distributed algorithms, generally known by the name of diffusing computations, that play an important role in all kinds distributed and/or database applications to perform tasks like termination detection, leader election, or propagation of information with feedback. We construct a highly parameterized abstract algorithm and shown that many existing algorithms and their applications can be obtained from this abstract algorithm by instantiating the parameters appropriately and/or refining some of its actions. Subsequently, we show that this use of parameterization and re-usability of notation and proof leads to a reduction of the effort and cost of developing and verifying distributed diffusing computations. More specific, we show that proving the correctness of any application now boils down to verifying an application-specific safety property and reusing the termination and safety proofs of the underlying abstract algorithm.

Keywords: Parameterization, re-use, specifications, formal proof,
distributed algorithms, diffusing computations.


Received April, 29, 2005, Revised August, 22, 2005 , Editor: Mauricio Solar
Full paper, 14 pages [ PDF, 456 Kb ]