Verification of the ring algorithm for distributed systems using the specification language of the temporal logic of actions
Abstract
Verification of the ring algorithm for distributed systems using the specification language of the temporal logic of actions
Incoming article date: 12.11.2025The article is devoted to the problem of verification of distributed algorithms using formal methods. The classical leader selection algorithm in ring topology, the ring algorithm, is chosen as the object of research. For its analysis, the specification language of the Temporal Logic of Actions (TLA+) is used. The paper presents a detailed formal model of the algorithm, describing its states and transitions, taking into account the features of distributed systems, such as the lack of shared memory. The key properties of correctness are formulated and proved: the uniqueness of the leader (the property of security), the finality of elections (the property of liveliness) and consent. The correctness of the specification was confirmed using the model model verifier of the language of temporal logic of actions, which exhaustively checked all achievable states for the model with three processes. The results demonstrate the effectiveness of the Time Logic Specification language (TLA+) for providing a high degree of confidence in the reliability of distributed systems.
Keywords: formal verification, distributed systems, ring algorithm, leader selection, specification language for temporal logic of actions, model verification, security properties, vivacity properties.formal verification, distributed systems, ring algorithm