Верификация алгоритма забияки для распределенных систем средствами TLA+ и PlusCal
Аннотация
Данная работа посвящена верификации алгоритма забияки для распределенных систем средствами TLA+ и PlusCal. В работе обзорно приводится основная информация о распределенных системах, далее приводится краткая информация о распределенных алгоритмах выбора координатора, и, затем приводится подробный разбор распределенного алгоритма забияки на простом примере распределенной системы из семи узлов. Затем, в работе демонстрируется созданная модель распределенного алгоритма забияки на языках спецификации TLA+ и PlusCal и приводится описание основных частей данной модели. Далее приводится верификация созданной модели. Верификация производится при помощи инструмента TLC – это специализированное средство проверки моделей и симулятор для TLA+ спецификаций. Далее в работе продемонстрирован результат верификации. В результате верификации распределенного алгоритма забияки удалось установить, что заявленные свойства надежности и живучести выполняются в полной мере для всех возможных состояний системы.
Это произведение доступно по лицензии Creative Commons «Attribution» («Атрибуция») 4.0 Всемирная.
Редакционная политика журнала основывается на традиционных этических принципах российской научной периодики и строится с учетом этических норм работы редакторов и издателей, закрепленных в Кодексе поведения и руководящих принципах наилучшей практики для редактора журнала (Code of Conduct and Best Practice Guidelines for Journal Editors) и Кодексе поведения для издателя журнала (Code of Conduct for Journal Publishers), разработанных Комитетом по публикационной этике - Committee on Publication Ethics (COPE). В процессе издательской деятельности редколлегия журнала руководствуется международными правилами охраны авторского права, нормами действующего законодательства РФ, международными издательскими стандартами и обязательной ссылке на первоисточник.
Журнал позволяет авторам сохранять авторское право без ограничений. Журнал позволяет авторам сохранить права на публикацию без ограничений.
Издательская политика в области авторского права и архивирования определяются «зеленым цветом» в базе данных SHERPA/RoMEO.
Все статьи распространяются на условиях лицензии Creative Commons «Attribution» («Атрибуция») 4.0 Всемирная, которая позволяет другим использовать, распространять, дополнять эту работу с обязательной ссылкой на оригинальную работу и публикацию в этом журналe.
