Distributed algorithms and their verification with Byzantine model checker

Abstract

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).