Revisiting Snapshot Algorithms by Refinement-based Techniques (Extended Version)

Abstract : 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-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 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.
Type de document :
Article dans une revue
Computer Science and Information Systems, ComSIS Consortium, 2014, Computer Science and Information System, 11 (1), pp.251-270. 〈http://www.comsis.org/archive.php?show=pprpdcat1〉. 〈10.2298/CSIS130122007A〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00924525
Contributeur : Manamiary Bruno Andriamiarina <>
Soumis le : lundi 6 janvier 2014 - 21:54:31
Dernière modification le : dimanche 12 novembre 2017 - 01:07:37

Identifiants

Collections

Citation

Manamiary Bruno Andriamiarina, Dominique Méry, Neeraj Kumar Singh. Revisiting Snapshot Algorithms by Refinement-based Techniques (Extended Version). Computer Science and Information Systems, ComSIS Consortium, 2014, Computer Science and Information System, 11 (1), pp.251-270. 〈http://www.comsis.org/archive.php?show=pprpdcat1〉. 〈10.2298/CSIS130122007A〉. 〈hal-00924525〉

Partager

Métriques

Consultations de la notice

334