Revisiting Snapshot Algorithms by Refinement-based Techniques

Manamiary Bruno Andriamiarina1, Dominique Méry1 and Neeraj Kumar Singh2

  1. Université de Lorraine, LORIA
    Vandoeuvre-lès-Nancy, France
    {Manamiary.Andriamiarina, Dominique.Mery}@loria.fr
  2. McMaster Centre for Software Certification, McMaster University
    Hamilton, Ontario, Canada
    singhn10@mcmaster.ca

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-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.

Key words

Distributed algorithms, correctness-by-construction, refinement, snapshot, verification

Digital Object Identifier (DOI)

https://doi.org/10.2298/CSIS130122007A

Publication information

Volume 11, Issue 1 (January 2014)
Year of Publication: 2014
ISSN: 2406-1018 (Online)
Publisher: ComSIS Consortium

Full text

DownloadAvailable in PDF
Portable Document Format

How to cite

Andriamiarina, M. B., Méry, D., Singh, N. K.: Revisiting Snapshot Algorithms by Refinement-based Techniques. Computer Science and Information Systems, Vol. 11, No. 1, 251–270. (2014), https://doi.org/10.2298/CSIS130122007A