Verification of the Bully Election Algorithm for Distributed Systems Using TLA+ and PlusCal

Abstract

This article is devoted to verification of the bully election algorithm for distributed systems with TLA+ and PlusCal. In this work, we show an overview of the basic information about distributed systems, then we show definition of election algorithms for distributed systems, after that we provide a full description of the bully election algorithm for distributed systems. Later in this article, we show the model of the distributed algorithm created with TLA+ and PlusCal. Then we describe the main parts of this model. Next, we illustrate results of verification of this model. The verification was done using TLC ‒ a model checker and simulator for executable TLA+ specifications. As a result of the verification, it was possible to establish that the declared properties of safety and liveness are fully satisfied for all possible states of the system.

Keywords

• coordinator election algorithm
• leader election algorithm
• bully algorithm
• distributed systems
• distributed computing
• formal verification
• specification language
• temporal logic
• model checking
• tla+
• pluscal
• tlc
• ltl