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

[[File:{{#setmainimage:Построение и верификация отказоустойчивого алгоритма распределенной блокировки (Евгений Шишкин, OSDAY-2018)!.jpg}}|center|640px]]
{{LinksSection}}

* 
<!-- <blockquote>[©]</blockquote> -->

{{vklink|1093}}                                          
{{fblink|2086022238317453}}                                          
<references/>

<!-- topub -->


{{stats|disqus_comments=0|refresh_time=2018-2019-02-21T19:33:11.998605-19T21:42:06.240263|vimeo_plays=910|youtube_comments=0|youtube_plays=1932}}

[[Категория:OSDAY-2018]]
[[Категория:Алгоритмы]]
[[Категория:Верификация]]

Версия 16:33, 21 февраля 2019

Докладчик

Евгений Шишкин

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

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

Видео

Презентация

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

• Discuss on VK
• Discuss on Facebook

Plays:42   Comments:0