The 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

The article explores the actor model as implemented in the Elixir programming language, which builds upon the principles of the Erlang language. The actor model is an approach to parallel programming where independent entities, called actors, communicate with each other through asynchronous messages. The article details the main concepts of Elixir, such as comparison with a sample, data immutability, types and collections, and mechanisms for working with the actors. Special attention is paid to the practical aspects of creating and managing actors, their interaction and maintenance. This article will be valuable for researchers and developers interested in parallel programming and functional programming languages.

Keywords: actor model, elixir, parallel programming, pattern matching, data immutability, processes, messages, mailbox, state, recursion, asynchrony, distributed systems, functional programming, fault tolerance, scalability