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

The growing popularity of large language models in various fields of scientific and industrial activity leads to the emergence of solutions using these technologies for completely different tasks. This article suggests using the BERT, GPT, and GPT-2 language models to detect malicious code. The neural network model, previously trained on natural texts, is further trained on a preprocessed dataset containing program files with malicious and harmless code. The preprocessing of the dataset consists in the fact that program files in the form of machine instructions are translated into a textual description in a formalized language. The model trained in this way is used for the task of classifying software based on the indication of the content of malicious code in it. The article provides information about the conducted experiment on the use of the proposed model. The quality of this approach is evaluated in comparison with existing antivirus technologies. Ways to improve the characteristics of the model are also suggested.

Keywords: antivirus, neural network, language models, malicious code, machine learning, model training, fine tuning, BERT, GPT, GPT-2

The paper analyzes various approaches to identifying and recognizing license plates in intelligent transport networks. A deep learning model has been proposed for localizing and recognizing license plates in natural images, which can achieve satisfactory results in terms of recognition accuracy and speed compared to traditional ones. Evaluations of the effectiveness of the deep learning model are provided.

Keywords: VANET, intelligent transport networks, YOLO, city traffic management system, steganography, deep learning, deep learning, information security, convolutional neural network, CNN

This article discusses modeling of polymer corrosion in aggressive environments based on percolation theory. Within the framework of the work, an algorithm for modeling polymer corrosion was developed, and a program that implements this algorithm in C ++. Paper describes the corrosion modeling algorithm, the structure of the implemented program, and the simulation results for various parameters. The result of this work is an algorithm modeling and an application that performs modeling of the polymer corrosion process in aggressive environments based on the percolation theory according to the developed algorithm, as well as building an image of the damaged material, graphs of the dependence of the length of the boundary of the corrosion region and the area of the remaining material on the modeling step. Algorithm uses Monte-Carlo method for determing area of corrosing region and is suitable for parallel implementation.

Keywords: percolation theory, corrosion modeling, simulation of physical processes, Monte Carlo method, visualization of simulation results