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

##plugins.themes.academic_pro.article.sidebar##

Published Mar 1, 2016
https://doi.org/10.47164/ijngc.v7i1.102
Download
pdf
Statistic

Downloads

Download data is not yet available.

Metrics

Metrics Loading ...
Volume 7, Issue 1, March 2016

##plugins.themes.academic_pro.article.main##

Alireza Souri
Department of Computer Engineering,Hadishahr Branch,Islamic Azad University, Hadishahr,Iran

Abstract

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.

##plugins.themes.academic_pro.article.details##

How to Cite
Alireza Souri. (2016). Formal Specification and Verification of a Data Replication Approach in Distributed Systems. International Journal of Next-Generation Computing, 7(1), 18–37. https://doi.org/10.47164/ijngc.v7i1.102
Crossref
Scopus
Google Scholar
Europe PMC

References

  1. Abawajy, J. and Mat Deris, M. 2013. Data Replication Approach with Data Consistency Guarantee for Data Grid. Computers, IEEE Transactions on PP, 99, 1.
  2. Alami Milani, B. and Jafari Navimipour, N. 2016. A comprehensive review of the data replication techniques in the cloud environments: Major trends and future directions. Journal of Network and Computer Applications 64, 229–238.
  3. Armendariz-Inigo, J. E., de Mend’ivil, J. R., Garitagoitia, J. R., and Munoz-Escoli, F. D. 2009. Correctness proof of a database replication protocol under the perspective of the I/O automaton model. Acta Informatica 46, 4, 297–330.
  4. Clarke Jr., E. M., Grumberg, O., and Peled, D. A. 1999. Model Checking. MIT Press, Cambridge, MA, USA. Dwyer, M. B., Avrunin, G. S., and Corbett, J. C. 1998. Property Specification Patterns for Finite-state Verification. In Proceedings of the Second Workshop on Formal Methods in Software Practice. FMSP ’98. ACM, New York, NY, USA, 7–15.
  5. Garcia, R., Rodrigues, R., and Preguic¸a, N. 2011. Efficient Middleware for Byzantine Fault Tolerant Database Replication. In Proceedings of the Sixth Conference on Computer Systems. EuroSys ’11. ACM, New York, NY, USA, 107–122.
  6. Garcia-Garcia, J., Ordonez, C., and Tosic, P. T. 2012. Efficiently repairing and measuring replica consistency in distributed databases. Distributed and Parallel Databases 31, 3, 377–411.
  7. Gray, J. and Reuter, A. 1992. Transaction Processing: Concepts and Techniques, 1st ed. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA.
  8. Hammal, Y., Ben-Othman, J., Mokdad, L., and Abdelli, A. 2015. Formal Modeling of Greedy Nodes in 802.15.4 WSN. ICT Express 1, 1 (jun), 10–13.
  9. Hansen, H., Virtanen, H., and Valmari, A. 2003. Merging State-Based and Action-Based Verification. In Proceedings of the Third International Conference on Application of Concurrency to System Design. ACSD ’03. IEEE Computer Society, Washington, DC, USA, 150—-.
  10. Holzmann, G. J. 1997. The model checker SPIN. IEEE Transactions on Software Engineering 23, 5, 279–295.
  11. Jafari Navimipour, N., Habibizad Navin, A., Rahmani, A. M., and Hosseinzadeh, M. 2015. Behavioral modeling and automated verification of a Cloud-based framework to share the knowledge and skills of human resources. Computers in Industry 68, 65–77.
  12. Kemme, B. and Alonso, G. 2000. A New Approach to Developing and Implementing Eager Database Replication Protocols. ACM Trans. Database Syst. 25, 3 (sep), 333–379.
  13. Liu, Y., Sun, J., and Dong, J. S. 2010. Automated Technology for Verification and Analysis: 8th International Symposium, ATVA 2010, Singapore, September 21-24, 2010. Proceedings. Springer Berlin Heidelberg, Berlin, Heidelberg, Chapter Developing, 371–377.
  14. Manna, Z. and Pnueli, A. 1995. Temporal Verification of Reactive Systems: Safety. Springer-Verlag New York, Inc., New York, NY, USA.
  15. McMillan, K. L. 1992. Symbolic Model Checking: An Approach to the State Explosion Problem. Ph.D. thesis, Pittsburgh, PA, USA.
  16. Perez, J. M., Garcia-Carballeira, F., Carretero, J., Calderon, A., and Fernandez, J. 2010. Branch replication scheme: A new model for data replication in large scale data grids. Future Generation Computer Systems 26, 1 (jan), 12–20.
  17. Poledna, S. 1994. Replica determinism in distributed real-time systems: A brief survey. Powell, D. 1994. Distributed Fault Tolerance - Lessons Learned from Delta-4. In Revised Papers from a Workshop on Hardware and Software Architectures for Fault Tolerance. Springer-Verlag, London, UK, UK, 199–217.
  18. Safarkhanlou, A., Souri, A., Norouzi, M., and Sardroud, S. E. H. 2015. Formalizing and Verification of an Antivirus Protection Service using Model Checking. In Procedia Computer Science. Vol. 57. Elsevier, 1324–1331.
  19. Schneider, F. B. 1990. Implementing Fault-tolerant Services Using the State Machine Approach: A Tutorial. ACM Comput. Surv. 22, 4 (dec), 299–319.
  20. Sciascia, D. and Pedone, F. 2013. Geo-replicated storage with scalable deferred update replication. In Proceedings of the International Conference on Dependable Systems and Networks.
  21. Souri, A. and Jafari Navimipour, N. 2014. Behavioral modeling and formal verification of a resource discovery approach in Grid computing. Expert Systems with Applications 41, 8, 3831–3849.
  22. Souri, A. and Norouzi, M. 2015. A new probable decision making approach for verification of probabilistic real-time systems.
  23. Souri, A. and Pashzadeh, S. 2014. CONSISTENCY OF Data Replication protocols in database Systems: A review. International Journal on Information Theory (IJIT) 3, 4, 19–32.
  24. Souri, A. and Rahmani, A. M. 2014. A survey for replica placement techniques in data grid environment. International Journal of Modern Education and Computer Science 6, 5, 46.
  25. Wiesmann, M., Pedone, F., Schiper, a., Kemme, B., and Alonso, G. 2000. Understanding replication in databases and distributed systems. Proceedings 20th IEEE International Conference on Distributed Computing Systems, 464–474.
  26. Zhu, Y. and Wang, J. 2010. Client-centric consistency formalization and verification for system with large-scale distributed data storage. Future Generation Computer Systems 26, 8 (oct), 1180–1188.