Abstract:  Consensus protocol is important element and core component of distributed system， it is dedicated to solve the problem of ensuring the same data consistency among nodes that may fail in a distributed scenario， and its accuracy and efficiency directly determine the performance of the system. Raft consensus protocol is common and effective consensus algorithm in current distributed systems. This paper firstly models the Raft consensus protocol formally using a probabilistic model detection method， then describes its relevant properties using property spcification technique of probabilistic model checking， and finally verifies and analyses the consistency and efficiency of the Raft consensus protocol. The experimental results show that it satisfies consistency， but the number of election rounds increases during the leader election phase when the difference range of the latest log serial numbers maintained by followers increases， resulting in the election time increase throughout the service cycle， thus affecting the execution efficiency of Raft.

Key words: distributed system, Raft consensus protocol, probabilistic model checking, formal verification, property specification