Никита Синяченко, Евгений Чернацкий — TLA+ для эффективного тестирования распределенных систем

Подробнее о конференции SmartData:
— — Скачать презентацию с сайта SmartData —
Распределенные системы очень сложно разрабатывать. Даже если агентов всего несколько, число различных состояний системы может превышать тысячи, а то и миллионы. На таких масштабах привычные методы тестирования бессмысленны, а число корнер-кейсов, которые могут возникнуть в случае некорректной реализации системы, вполне способно выйти за практические рамки. В докладе спикеры подробнее изучают проблему разработки и тестирования распределенных систем, рассмотрим язык спецификации TLA+ и его применение для верификации программ. Дополнительно описывается метод тестирования распределенных систем, построенных на акторной модели, совмещающий в себе плюсы и фаззинга, и TLA+. В качестве примера спикеры рассматривают систему распределенной координации Барсик, которая активно разрабатывается ВКонтакте и основана на алгоритме репликации данных Viewstamped Replication.