Revisiting Snapshot Algorithms by Refinement-based Techniques
Computer Science and Information Systems, Tome 11 (2014) no. 1
Cet article a éte moissonné depuis 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},
year = {2014},
volume = {11},
number = {1},
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 UR - http://geodesic.mathdoc.fr/item/CSIS_2014_11_1_a17/ ID - CSIS_2014_11_1_a17 ER -
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/