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

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