Using TLA+ to Specify Leader Election of Raft Algorithm with Consideration of Leadership Transfer in Multiple Controllers

the consistency problem can be solved by running the Raft consensus algorithm in a distributed cluster, but the re-election of the leader may cause the cluster to be unavailable. Therefore, the leadership transfer function is increased to the Raft algorithm to prevent the cluster unavailable because of the leader being shut down or removed from the cluster and so on. To cope with such situation, the leadership transfer function is formally specified with the TLA+ language and verified with the TLC Model Checker to prove its correctness. And then the codes of the leadership transfer implemented in OpenDaylight are analyzed. In the end, the measured time of reelection and time of leadership transfer proves that the availability of the cluster is heightened when the Leader is asked to shut down.