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.
Liste complète des métadonnées

https://hal.inria.fr/inria-00093164
Contributeur : Dominique Méry <>
Soumis le : mardi 12 septembre 2006 - 18:12:29
Dernière modification le : jeudi 17 mai 2018 - 12:52:03

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

219