Formalization and Verification of PaxosStore from Process Algebra Perspective

PaxosStore is a high-availability storage system developed to support the comprehensive business of WeChat. With the widespread application of WeChat, it is particularly important to verify the safety of PaxosStore. This work proposes a formal model for the storage system PaxosStore using the process algebra Communicating Sequential Processes (CSP) to clearly reflect the interactions of the components in PaxosStore. More importantly, we utilize the model checker Process Analysis Toolkit (PAT) to simulate and verify the constructed CSP model. We specifically verify the validity of six properties: deadlock-freeness, divergence-freeness, robustness, consistency, nontriviality and liveness. Through the verification results, we demonstrate that our formalization model successfully satisfies these properties, confirming the correctness and effectiveness of the framework in ensuring secure interactions among the PaxosStore storage system components.