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
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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
Liste complète des métadonnées

Cited literature [22 references]  Display  Hide  Download

https://hal.inria.fr/hal-00734131
Contributor : Manamiary Bruno Andriamiarina <>
Submitted on : Thursday, September 20, 2012 - 6:01:07 PM
Last modification on : Tuesday, February 19, 2019 - 3:40:03 PM
Document(s) archivé(s) le : Friday, December 21, 2012 - 3:51:29 AM

File

pdcat2012v14.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00734131, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

460

Files downloads

498