Построение и верификация отказоустойчивого алгоритма распределенной блокировки (Евгений Шишкин, OSDAY-2018) — различия между версиями
Материал из 0x1.tv
StasFomin (обсуждение | вклад) |
StasFomin (обсуждение | вклад) |
||
[[File:{{#setmainimage:Построение и верификация отказоустойчивого алгоритма распределенной блокировки (Евгений Шишкин, OSDAY-2018)!.jpg}}|center|640px]] {{LinksSection}} * <!-- <blockquote>[©]</blockquote> --> {{vklink|1093}} {{fblink|2086022238317453}} <references/> <!-- topub --> {{stats|disqus_comments=0|refresh_time=2020-07-18T23:55:582021-08-25T03:18:54.804312822265|vimeo_plays=1624|youtube_comments=1|youtube_plays=88113}} [[Категория:OSDAY-2018]] [[Категория:Алгоритмы]] [[Категория:Верификация]] |
Версия 00:18, 25 августа 2021
- Докладчик
- Евгений Шишкин
В работе демонстрируется применение гибридного подхода к верификации отказоустойчивого, адаптирующегося к изменению группы участников алгоритма распределенной блокировки на основе алгоритма Рикарта-Агравала. Для доказательства свойства надежности неотказоустойчивого ядра алгоритма используется формализация в системе доказательств Coq, в то время как оснастка, позволяющая стать алгоритму отказоустойчивым формализуется в TLA+ и проверяется на ограниченной модели. Результатом работы по-мимо расширения алгоритма, доказательств и модели стала реализация описанного отказоустойчивого алгоритма на языке Erlang.
Работа также ставит целью продемонстрировать способ использования некоторых современных средств верификации для построения высоконадежных компонент в контексте языка Erlang.
Видео
Посмотрели доклад? Понравился? Напишите комментарий! Не согласны? Тем более напишите.
Презентация
Примечания и ссылки
Plays:137
Comments:1