Построение и верификация отказоустойчивого алгоритма распределенной блокировки (Евгений Шишкин, OSDAY-2018) — различия между версиями
Материал из 0x1.tv
StasFomin (обсуждение | вклад) |
StasFomin (обсуждение | вклад) |
||
<!-- {{youtubelink|}} -->
{{SlidesSection}}
[[File:Построение и верификация отказоустойчивого алгоритма распределенной блокировки (Евгений Шишкин, OSDAY-2018).pdf|left|page=-|300px]]
{{----}}
[[File:{{#setmainimage:Построение и верификация отказоустойчивого алгоритма распределенной блокировки (Евгений Шишкин, OSDAY-2018)!.jpg}}|center|640px]]
{{LinksSection}}
*
<!-- <blockquote>[©]</blockquote> -->
{{vklink|107693}}
<references/>
<!-- topub -->
[[Категория:OSDAY-2018]] | |||
Версия 03:36, 26 июня 2018
- Докладчик
- Евгений Шишкин
В работе демонстрируется применение гибридного подхода к верификации отказоустойчивого, адаптирующегося к изменению группы участников алгоритма распределенной блокировки на основе алгоритма Рикарта-Агравала. Для доказательства свойства надежности неотказоустойчивого ядра алгоритма используется формализация в системе доказательств Coq, в то время как оснастка, позволяющая стать алгоритму отказоустойчивым формализуется в TLA+ и проверяется на ограниченной модели. Результатом работы по-мимо расширения алгоритма, доказательств и модели стала реализация описанного отказоустойчивого алгоритма на языке Erlang.
Работа также ставит целью продемонстрировать способ использования некоторых современных средств верификации для построения высоконадежных компонент в контексте языка Erlang.
Видео
Презентация
!.jpg)