Formal Specification and Verification of a Data Replication Approach in Distributed Systems

Data replication is an important optimization phase to manage large data by replicating data in various distributed systems. In distributed systems, reliability and performance are two important factors for using data replication. Also model checking techniques can be used to verify the correctness of these systems. In this paper, a Data Replication approach has been proposed. This paper presents a behavioral modeling the proposed approach with the goals of providing correctness and reducing verification time and memory consumption. Evaluating and analyzing the logical problems such as deadlock free, reachability and fairness for the considered data replication approach are provided. For verifying the behavioral models of the proposed data replication approach the NuSMV model checker is employed. The verification results are compared by user graphical interface and Kripke model verification methods.