Евгений Шишкин, ведущий исследователь, научный отдел компании ИнфоТеКС.
Выпускник МГТУ им. Н.Э.Баумана, специальность: прикладная математика. Проработав в индустрии около 10 лет в роли системного программиста и разработчика распределенных систем, ежедневно наблюдая колоссальную сложность конструируемых механизмов, Евгений всерьез заинтересовался методами строго обоснования надежности разрабатываемых систем. С 2016 г. Евгений занимает должность ведущего исследователя в научном отделе компании ИнфоТеКС. Основной исследовательский интерес: Формальные доказательства корректности ПО, методы составления формальных спецификаций на системы.
В работе демонстрируется применение гибридного подхода к верификации отказоустойчивого, адаптирующегося к изменению группы участников алгоритма распределенной блокировки на основе алгоритма Рикарта-Агравала.
Для доказательства свойства надежности неотказоустойчивого ядра алгоритма используется формализация в системе доказательств Coq, в то время как оснастка, позволяющая стать алгоритму отказоустойчивым формализуется в TLA+ и проверяется на ограниченной модели. Результатом работы по-мимо расширения алгоритма, доказательств и модели стала реализация описанного отказоустойчивого алгоритма на языке Erlang.
Работа также ставит целью продемонстрировать способ использования некоторых современных средств верификации для построения высоконадежных компонент в контексте языка Erlang.
