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

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

(Batch edit: replace PCRE (\n\n)+(\n) with \2)
 
(не показаны 4 промежуточные версии этого же участника)
;{{SpeakerInfo}}: {{Speaker|Евгений Шишкин}}
<blockquote>
В работе демонстрируется применение гибридного подхода к верификации отказоустойчивого, адаптирующегося к изменению группы участников алгоритма распределенной блокировки на основе алгоритма Рикарта-Агравала. Для доказательства свойства надежности неотказоустойчивого ядра алгоритма используется формализация в системе доказательств Coq, в то время как оснастка, позволяющая стать алгоритму отказоустойчивым формализуется в TLA+ и проверяется на ограниченной модели. Результатом работы по-мимо расширения алгоритма, доказательств и модели стала реализация описанного отказоустойчивого алгоритма на языке Erlang.

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

{{VideoSection}}
{{vimeoembed|240323112|800|450}}

{{youtubelink|Z-vjvz7E5NY}}{{letscomment}}


{{SlidesSection}}
[[File:Построение и верификация отказоустойчивого алгоритма распределенной блокировки (Евгений Шишкин, OSDAY-2018).pdf|left|page=-|300px]]

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

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

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

<!-- topub -->


{{stats|disqus_comments=0|refresh_time=2020-07-06T20:35:122021-08-31T17:54:50.341342793498|vimeo_plays=1624|youtube_comments=1|youtube_plays=87113}}

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

Текущая версия на 12:22, 4 сентября 2021

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

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

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

Видео

on youtube

Посмотрели доклад? Понравился? Напишите комментарий! Не согласны? Тем более напишите.

Презентация

Построение и верификация отказоустойчивого алгоритма распределенной блокировки (Евгений Шишкин, 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

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


Plays:137   Comments:1