Search

Данная работа посвящена верификации алгоритма забияки для распределенных систем средствами TLA+ и PlusCal. В работе обзорно приводится основная информация о распределенных системах, далее приводится краткая информация о распределенных алгоритмах выбора координатора, и, затем приводится подробный разбор распределенного алгоритма забияки на простом примере распределенной системы из семи узлов. Затем, в работе демонстрируется созданная модель распределенного алгоритма забияки на языках спецификации TLA+ и PlusCal и приводится описание основных частей данной модели. Далее приводится верификация созданной модели. Верификация производится при помощи инструмента TLC – это специализированное средство проверки моделей и симулятор для TLA+ спецификаций. Далее в работе продемонстрирован результат верификации. В результате верификации распределенного алгоритма забияки удалось установить, что заявленные свойства надежности и живучести выполняются в полной мере для всех возможных состояний системы., 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., Международный научный журнал "Современные информационные технологии и ИТ-образование", Выпуск 1 2022, Pages 54-61