Distributed algorithms and their verification with Byzantine model checker
Keywords:
distributed algorithms, parallel program, ByMC, model checking, verificationAbstract
Every system algorithms are the main nodes for the construction of reliable distributed systems. To ensure that these algorithms make the system more reliable, we have to ensure that the proposed algorithms are working properly. However, check the model implemented fault tolerance of distributed algorithms [1] in real can be used for very small systems only. To finally, be able to automatically check the fault-tolerant distributed algorithms on large systems. Since they are aimed at improving the reliability of computer systems, it is important that these algorithms are correct and fully satisfy their requirements. Due to different sources of non-determinism is easy to fail in the arguments of the correctness of distributed algorithms on the level of temporality. Therefore, they are unreliable material for model checking. Nevertheless, the model checking method for distributed fault-tolerant algorithm is extremely difficult work. In this article we will discuss the modeling and verification of algorithm Broadcast "Parsing"by broadcasting [2] with Spin and ByMC (Byzantine Model Checker [3]). The proposed properties are safety and liveness in the LTL(Linear-temporal logic).
References
[2] Srikanth T., Toueg S. Simulating authenticated broadcasts to derive simple fault-tolerant algorithms. // Distributed Computing 2, - 1987. - P. 80–94.
[3] John A., Konnov I., Schmid U., Veith H., Widder J. Counter Attack on Byzantine Generals: Parameterized Model Checking of Fault-tolerant Distributed Algorithms. // Cornell University Library. Ithaca. NY. - V2. - 2013. - P. 56-75.
[4] Miner D., Shook A. MapReduce Design Patterns. Building Effective Algorithms and Analytics for Hadoop and Other Systems. // Ottawa. Canada. ACM. NY. - 2012. – P. 204–213.
[5] Akhmed-Zaki D.Zh., Bektemessov A.T. Simulation of distributed programm with transactional memory. // Buletin KazNU. Almaty – 2014. – P. 26-33.
[6] Charron-Bost B., Pedone F., Schiper A. Replication: Theory and Practice // Lecture Notes in Computer Science. Springer. - V 5959. - 2010. - P. 156-167.
[7] Bokor P., Kinder J., Serafini M., Suri N. Efficient model checking of fault-tolerant distributed protocols. // In: DSN. - 2011. - P. 73–84.
[8] Clarke E. M., Grumberg O., Peled D.A. Model Checking // The MIT Press. London. England. - 1999. –330 p.
[9] John A., Konnov I., Schmid U., Veith H., Widder J. Starting a dialog between model checking and fault-tolerant distributed algorithms // arXiv CoRR abs/1210.3839. - 2012.
[10] Aubakirov S., Trigo P. and Ahmed-Zaki D. Comparison of Distributed Computing Approaches to Complexity of n-gram Extraction // Agent and Systems Modeling, Portugal Proceedings of DATA, - 2016. –P. 25–30.
[11] Clarke E., Grumberg O., Jha S., Lu Y., Veith H. Counterexample-guided abstraction refinement for symbolic model checking. // J.ACM 50(5). - 2003. - P. 752–794
[12] Benchmarks Spin2013 ByMC 0.9.5: Byzantine model checker, http://forsyte.tuwien.ac.at/software/bymc/ (Application date: 05.08.2016)
