Верификация алгоритма забияки для распределенных систем средствами TLA+ и PlusCal

Аннотация

Данная работа посвящена верификации алгоритма забияки для распределенных систем средствами TLA+ и PlusCal. В работе обзорно приводится основная информация о распределенных системах, далее приводится краткая информация о распределенных алгоритмах выбора координатора, и, затем приводится подробный разбор распределенного алгоритма забияки на простом примере распределенной системы из семи узлов. Затем, в работе демонстрируется созданная модель распределенного алгоритма забияки на языках спецификации TLA+ и PlusCal и приводится описание основных частей данной модели. Далее приводится верификация созданной модели. Верификация производится при помощи инструмента TLC – это специализированное средство проверки моделей и симулятор для TLA+ спецификаций. Далее в работе продемонстрирован результат верификации. В результате верификации распределенного алгоритма забияки удалось установить, что заявленные свойства надежности и живучести выполняются в полной мере для всех возможных состояний системы.

Сведения об авторах

Aleksey Sergeevich Polyakov, Кубанский государственный университет

магистрант кафедры вычислительных технологий, факультет компьютерных технологий и прикладной математики

Elisey Alekseevich Nigodin, Кубанский государственный университет

магистрант кафедры вычислительных технологий, факультет компьютерных технологий и прикладной математики

Elena Evgenievna Polupanova, Кубанский государственный университет

доцент кафедры вычислительных технологий, факультет компьютерных технологий и прикладной математики, кандидат технических наук

Pavel Evgenievich Usov, Кубанский государственный университет

магистрант кафедры вычислительных технологий, факультет компьютерных технологий и прикладной математики

Опубликована
2022-03-31
Как цитировать
POLYAKOV, Aleksey Sergeevich et al. Верификация алгоритма забияки для распределенных систем средствами TLA+ и PlusCal. Международный научный журнал «Современные информационные технологии и ИТ-образование», [S.l.], v. 18, n. 1, mar. 2022. ISSN 2411-1473. Доступно на: <http://sitito.cs.msu.ru/index.php/SITITO/article/view/817>. Дата доступа: 04 july 2022
Раздел
Параллельное и распределенное программирование, грид-технологии