Skip to Main content Skip to Navigation
Journal articles

Formal and Incremental Construction of Distributed Algorithms: On the Distributed Reference Counting Algorithm

Dominique Cansell 1, 2 Dominique Méry 1
1 MOSEL - Proof-oriented development of computer-based systems
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : The development of distributed algorithms and, more generally, distributed systems, is a complex, delicate and challenging process. Refinement techniques of (system) models improve the process by using a proof assistant, and by applying a design methodology aimed at starting from the most abstract model and leading, in an incremental way, to the most concrete model, for producing a distributed solution. We show, using the distributed reference counting (DRC) problem as our study, how models can be produced in an elegant and progressive way, thanks to the refinement and how the final distributed algorithm is built starting from these models. The development is carried out within the framework of the event B method and models are validated with a proof assistant.
Complete list of metadata

https://hal.inria.fr/inria-00093164
Contributor : Dominique Méry <>
Submitted on : Tuesday, September 12, 2006 - 6:12:29 PM
Last modification on : Friday, February 26, 2021 - 3:28:05 PM

Identifiers

  • HAL Id : inria-00093164, version 1

Collections

Citation

Dominique Cansell, Dominique Méry. Formal and Incremental Construction of Distributed Algorithms: On the Distributed Reference Counting Algorithm. Theoretical Computer Science, Elsevier, 2006. ⟨inria-00093164⟩

Share

Metrics

Record views

290