Верификация алгоритма кольца для распределённых систем с использованием языка спецификаций временной логики действий

Аннотация

Шиян В.И., Кузнецов А.М., Литвиненко П.Н., Полтавская А.А., Прохоров М.А., Степуленко К.А., Токарева Д.С.

Дата поступления статьи: 12.11.2025

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

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

1.2.2 - Математическое моделирование, численные методы и комплексы программ

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