Skip to Main content Skip to Navigation
Conference papers

Revisiting Snapshot Algorithms by Refinement-based Techniques

Manamiary Bruno Andriamiarina 1, 2 Dominique Méry 1 Neeraj Kumar Singh 1
1 MOSEL - Proof-oriented development of computer-based systems
LORIA - FM - Department of Formal Methods
2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
LORIA - FM - Department of Formal Methods , Inria Nancy - Grand Est, MPII - Max-Planck-Institut für Informatik
Abstract : The snapshot problem addresses a collection of important algorithmic issues related to the distributed computations, which are used for debugging or recovering the distributed programs. Among the existing solutions, Chandy and Lamport propose a simple distributed algorithm. In this paper, we explore the correct-by-construction 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 a correct distributed algorithm. Moreover, we demonstrate how this class of other distributed algorithms can be revisited. A consequence is to provide a fully mechanized proof of the distributed algorithms.
Document type :
Conference papers
Complete list of metadata

Cited literature [22 references]  Display  Hide  Download
Contributor : Manamiary Bruno Andriamiarina Connect in order to contact the contributor
Submitted on : Thursday, September 20, 2012 - 6:01:07 PM
Last modification on : Saturday, October 16, 2021 - 11:26:09 AM
Long-term archiving on: : Friday, December 21, 2012 - 3:51:29 AM


Files produced by the author(s)


  • HAL Id : hal-00734131, version 1



Manamiary Bruno Andriamiarina, Dominique Méry, Neeraj Kumar Singh. Revisiting Snapshot Algorithms by Refinement-based Techniques. PDCAT 2012 : The Thirteenth International Conference on Parallel and Distributed Computing, Applications and Technologies, Dec 2012, Beijing, China. ⟨hal-00734131⟩



Les métriques sont temporairement indisponibles