Статья посвящена проблеме верификации распределённых алгоритмов с использованием формальных методов. В качестве объекта исследования выбран классический алгоритм выбора лидера в кольцевой топологии – алгоритм кольца. Для его анализа применяется язык спецификаций временной логики действий (Temporal Logic of Actions – TLA+). В работе представлена детальная формальная модель алгоритма, описывающая его состояния и переходы с учётом особенностей распределённых систем, таких как отсутствие разделяемой памяти. Формулируются и доказываются ключевые свойства корректности: уникальность лидера (свойство безопасности), завершаемость выборов (свойство живости) и согласие. Корректность спецификации подтверждена с помощью модельного верификатора моделей языка временной логики действий, который исчерпывающе проверил все достижимые состояния для модели с тремя процессами. Результаты демонстрируют эффективность языка спецификаций временной логики действий (TLA+) для обеспечения высокой степени уверенности в надёжности распределённых систем.

Ключевые слова: формальная верификация, распределённые системы, алгоритм кольца, выбор лидера, язык спецификаций временной логики действий, проверка моделей, свойства безопасности, свойства живости

1.2.2 - Математическое моделирование, численные методы и комплексы программ , 2.3.1 - Системный анализ, управление и обработка информации

В статье рассматривается акторная модель, реализованная в языке программирования Elixir, который является наследником языка Erlang. Акторная модель представляет собой подход к параллельному программированию, где независимые объекты, называемые акторами, взаимодействуют друг с другом посредством асинхронных сообщений. В статье подробно описаны основные концепции Elixir, такие как сопоставление с образцом, неизменяемость данных, типы и коллекции, а также механизмы работы с акторами. Особое внимание уделено практическим аспектам создания и управления акторами, их взаимодействию и поддержанию состояния. Статья будет полезна исследователям и разработчикам, интересующимся параллельным программированием и функциональными языками.

Ключевые слова: акторная модель, elixir, параллельное программирование, сопоставление с образцом, неизменяемость данных, процессы, сообщения, почтовый ящик, состояние, рекурсия, асинхронность, распределённые системы, функциональное программирование, отказоустойчивость

1.2.2 - Математическое моделирование, численные методы и комплексы программ , 2.3.1 - Системный анализ, управление и обработка информации