Formal Specification and Verification of CRDTs

Abstract : Convergent Replicated Data Types (CRDTs) can be used as basic building blocks for storing and managing replicated data in a distributed system. They provide high availability and performance, and they guarantee eventual consistency. In this paper, we develop a formal framework for the analysis and verification of CRDTs. We investigate and compare the three currently used specification techniques for CRDTs and formalize them based on an abstract model for managing replicated data in distributed systems. We show how CRDT implementations can be expressed in our framework and present a general strategy for verifying CRDTs. Finally, we report on our experiences in using the framework for the verification of important existing CRDT implementations. The framework and the proofs were developed within the interactive theorem prover Isabelle/HOL.
Type de document :
Communication dans un congrès
Erika Ábrahám; Catuscia Palamidessi. 34th Formal Techniques for Networked and Distributed Systems (FORTE), Jun 2014, Berlin, Germany. Springer, Lecture Notes in Computer Science, LNCS-8461, pp.33-48, 2014, Formal Techniques for Distributed Objects, Components, and Systems. 〈10.1007/978-3-662-43613-4_3〉
Liste complète des métadonnées

Littérature citée [15 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01398007
Contributeur : Hal Ifip <>
Soumis le : mercredi 16 novembre 2016 - 15:34:05
Dernière modification le : mercredi 16 novembre 2016 - 16:23:24
Document(s) archivé(s) le : jeudi 16 mars 2017 - 14:43:16

Fichier

978-3-662-43613-4_3_Chapter.pd...
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Peter Zeller, Annette Bieniusa, Arnd Poetzsch-Heffter. Formal Specification and Verification of CRDTs. Erika Ábrahám; Catuscia Palamidessi. 34th Formal Techniques for Networked and Distributed Systems (FORTE), Jun 2014, Berlin, Germany. Springer, Lecture Notes in Computer Science, LNCS-8461, pp.33-48, 2014, Formal Techniques for Distributed Objects, Components, and Systems. 〈10.1007/978-3-662-43613-4_3〉. 〈hal-01398007〉

Partager

Métriques

Consultations de la notice

43

Téléchargements de fichiers

49