Построение и верификация отказоустойчивого алгоритма распределенной блокировки (Евгений Шишкин, OSDAY-2018)

Материал из 0x1.tv

Докладчик
Евгений Шишкин.jpg
Евгений Шишкин

В работе демонстрируется применение гибридного подхода к верификации отказоустойчивого, адаптирующегося к изменению группы участников алгоритма распределенной блокировки на основе алгоритма Рикарта-Агравала. Для доказательства свойства надежности неотказоустойчивого ядра алгоритма используется формализация в системе доказательств Coq, в то время как оснастка, позволяющая стать алгоритму отказоустойчивым формализуется в TLA+ и проверяется на ограниченной модели. Результатом работы по-мимо расширения алгоритма, доказательств и модели стала реализация описанного отказоустойчивого алгоритма на языке Erlang.

Работа также ставит целью продемонстрировать способ использования некоторых современных средств верификации для построения высоконадежных компонент в контексте языка Erlang.

Видео

Презентация

Построение и верификация отказоустойчивого алгоритма распределенной блокировки (Евгений Шишкин, OSDAY-2018).pdf Построение и верификация отказоустойчивого алгоритма распределенной блокировки (Евгений Шишкин, OSDAY-2018).pdf Построение и верификация отказоустойчивого алгоритма распределенной блокировки (Евгений Шишкин, OSDAY-2018).pdf Построение и верификация отказоустойчивого алгоритма распределенной блокировки (Евгений Шишкин, OSDAY-2018).pdf Построение и верификация отказоустойчивого алгоритма распределенной блокировки (Евгений Шишкин, OSDAY-2018).pdf Построение и верификация отказоустойчивого алгоритма распределенной блокировки (Евгений Шишкин, OSDAY-2018).pdf Построение и верификация отказоустойчивого алгоритма распределенной блокировки (Евгений Шишкин, OSDAY-2018).pdf Построение и верификация отказоустойчивого алгоритма распределенной блокировки (Евгений Шишкин, OSDAY-2018).pdf Построение и верификация отказоустойчивого алгоритма распределенной блокировки (Евгений Шишкин, OSDAY-2018).pdf Построение и верификация отказоустойчивого алгоритма распределенной блокировки (Евгений Шишкин, OSDAY-2018).pdf Построение и верификация отказоустойчивого алгоритма распределенной блокировки (Евгений Шишкин, OSDAY-2018).pdf Построение и верификация отказоустойчивого алгоритма распределенной блокировки (Евгений Шишкин, OSDAY-2018).pdf Построение и верификация отказоустойчивого алгоритма распределенной блокировки (Евгений Шишкин, OSDAY-2018).pdf Построение и верификация отказоустойчивого алгоритма распределенной блокировки (Евгений Шишкин, OSDAY-2018).pdf Построение и верификация отказоустойчивого алгоритма распределенной блокировки (Евгений Шишкин, OSDAY-2018).pdf Построение и верификация отказоустойчивого алгоритма распределенной блокировки (Евгений Шишкин, OSDAY-2018).pdf Построение и верификация отказоустойчивого алгоритма распределенной блокировки (Евгений Шишкин, OSDAY-2018).pdf Построение и верификация отказоустойчивого алгоритма распределенной блокировки (Евгений Шишкин, OSDAY-2018).pdf Построение и верификация отказоустойчивого алгоритма распределенной блокировки (Евгений Шишкин, OSDAY-2018).pdf Построение и верификация отказоустойчивого алгоритма распределенной блокировки (Евгений Шишкин, OSDAY-2018).pdf Построение и верификация отказоустойчивого алгоритма распределенной блокировки (Евгений Шишкин, OSDAY-2018).pdf
Построение и верификация отказоустойчивого алгоритма распределенной блокировки (Евгений Шишкин, OSDAY-2018)!.jpg

Примечания и ссылки