Facilitating the Verification of Diffusing Computations and Their Applications

Tanja E. J. Vos (1), S. Doaitse S. Swierstra (2)

e-mails: tanja@iti.upv.es, doaitse@cs.uu.nl

(1) Universidad Politécnica de Valencia - Instituto Tecnológico de Informática Valencia España
(2) Informatica Instituut, University of Utrecht Utrecht Holanda

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 otation 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, Parameterization, Re-use, Specifications, Formal Proof, Distributed Algorithms, Diffusing Computations

BibTex

@INPROCEEDINGS{vos04:5,
                  AUTHOR       = {Tanja E. J. Vos and S. Doaitse S. Swierstra},
                  TITLE        = {Facilitating the Verification of Diffusing Computations and Their Applications},
                  BOOKTITLE    = {30ma Conferencia Latinoamericana de Informática (CLEI2004)},
                  YEAR         = {2004},
                  editor       = {Mauricio Solar and David Fernández-Baca and Ernesto Cuadros-Vargas},
                  pages        = {42--53},
                  address      = {},
                  month        = Sep,
                  organization = {Sociedad Peruana de Computación},
                  note         = {ISBN 9972-9876-2-0},
                  file         = {http://clei2004.spc.org.pe/es/html/pdfs/5.pdf}
}

PDF de este artículo
PDF de CLEI2004 (incluye todos los artículos)
Página principal CLEI 2004
Generado por Sociedad Peruana de Computación