Revisiting Snapshot Algorithms by Refinement-based Techniques
Computer Science and Information Systems, Tome 11 (2014) no. 1

Voir la notice de l'article provenant de la source Computer Science and Information Systems website

The snapshot problem addresses a collection of important algorithmic issues related to distributed computations, which are used for debugging or recovering distributed programs. Among existing solutions, Chandy and Lamport have proposed a simple distributed algorithm. In this paper, we explore the correct-byconstruction process to formalize the snapshot algorithms in distributed system. The formalization process is based on a modeling language Event B, which supports a refinement-based incremental development using RODIN platform. These refinement-based techniques help to derive correct distributed algorithms. Moreover, we demonstrate how other distributed algorithms can be revisited. A consequence is to provide a fully mechanized proof of the resulting distributed algorithms.
Keywords: Distributed algorithms, correctness-by-construction, refinement, snapshot, verification
@article{CSIS_2014_11_1_a17,
     author = {Manamiary Bruno Andriamiarina and Dominique M\'ery and Neeraj Kumar Singh},
     title = {Revisiting {Snapshot} {Algorithms} by {Refinement-based} {Techniques}},
     journal = {Computer Science and Information Systems},
     publisher = {mathdoc},
     volume = {11},
     number = {1},
     year = {2014},
     url = {http://geodesic.mathdoc.fr/item/CSIS_2014_11_1_a17/}
}
TY  - JOUR
AU  - Manamiary Bruno Andriamiarina
AU  - Dominique Méry
AU  - Neeraj Kumar Singh
TI  - Revisiting Snapshot Algorithms by Refinement-based Techniques
JO  - Computer Science and Information Systems
PY  - 2014
VL  - 11
IS  - 1
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/CSIS_2014_11_1_a17/
ID  - CSIS_2014_11_1_a17
ER  - 
%0 Journal Article
%A Manamiary Bruno Andriamiarina
%A Dominique Méry
%A Neeraj Kumar Singh
%T Revisiting Snapshot Algorithms by Refinement-based Techniques
%J Computer Science and Information Systems
%D 2014
%V 11
%N 1
%I mathdoc
%U http://geodesic.mathdoc.fr/item/CSIS_2014_11_1_a17/
%F CSIS_2014_11_1_a17
Manamiary Bruno Andriamiarina; Dominique Méry; Neeraj Kumar Singh. Revisiting Snapshot Algorithms by Refinement-based Techniques. Computer Science and Information Systems, Tome 11 (2014) no. 1. http://geodesic.mathdoc.fr/item/CSIS_2014_11_1_a17/