Formal Specification and Verification of a Data Replication Approach in Distributed Systems.
Alireza Souri · INTERNATIONAL JOURNAL OF NEXT-GENERATION COMPUTING · 2016
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 formal verification and model checking techniques can be used to verify the correctness of these systems. In this paper, a Combined Semi-Active Data Replication approach has been proposed. This paper presents a behavioral modeling for 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. To verification of the behavior models of data replication approach the NuSMV model checker is employed by two methods user graphical interface and Kripke model. Normal 0 false false false EN-US X-NONE AR-SA /* Style Definitions */ table.MsoNormalTable {mso-style-name:Table Normal; mso-tstyle-rowband-size:0; mso-tstyle-colband-size:0; mso-style-noshow:yes; mso-style-priority:99; mso-style-parent:; mso-padding-alt:0cm 5.4pt 0cm 5.4pt; mso-para-margin-top:0cm; mso-para-margin-right:0cm; mso-para-margin-bottom:10.0pt; mso-para-margin-left:0cm; line-height:115%; mso-pagination:widow-orphan; font-size:11.0pt; font-family:Calibri,sans-serif; mso-ascii-font-family:Calibri; mso-ascii-theme-font:minor-latin; mso-hansi-font-family:Calibri; mso-hansi-theme-font:minor-latin; mso-bidi-font-family:Arial; mso-bidi-theme-font:minor-bidi;}