%0 Conference Proceedings
%T Formalizing and Validating the P-Store Replicated Data Store in Maude
%+ University of Oslo (UiO)
%+ University of Illinois at Urbana-Champaign [Urbana] (UIUC)
%A Ölveczky, Peter, Csaba
%Z Part 4: Regular Papers
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 23th International Workshop on Algebraic Development Techniques (WADT)
%C Gregynog, United Kingdom
%Y Phillip James
%Y Markus Roggenbach
%I Springer International Publishing
%3 Recent Trends in Algebraic Development Techniques
%V LNCS-10644
%P 189-207
%8 2016-09-21
%D 2016
%R 10.1007/978-3-319-72044-9_13
%Z Computer Science [cs]Conference papers
%X P-Store is a well-known partially replicated transactional data store that combines wide-area replication, data partition, some fault tolerance, serializability, and limited use of atomic multicast. In addition, a number of recent data store designs can be seen as extensions of P-Store. This paper describes the formalization and formal analysis of P-Store using the rewriting logic framework Maude. As part of this work, this paper specifies group communication commitment and defines an abstract Maude model of atomic multicast, both of which are key building blocks in many data store designs. Maude model checking analysis uncovered a non-trivial error in P-Store; this paper also formalizes a correction of P-Store whose analysis did not uncover any flaw.
%G English
%Z TC 1
%Z WG 1.3
%2 https://inria.hal.science/hal-01767476/document
%2 https://inria.hal.science/hal-01767476/file/433330_1_En_13_Chapter.pdf
%L hal-01767476
%U https://inria.hal.science/hal-01767476
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-TC1
%~ IFIP-WG1-3
%~ IFIP-WADT
%~ IFIP-LNCS-10644