Реализация алгоритма Chord в виде акторной системы и формальная верификация этой реализации

Первушина Наталия Владимировна

Аннотация


Дипломная работа 79 с. 1 рис. 1 табл. 27 ист.
Гипотеза работы: сложность разработки можно значительно уменьшить, описывая распределенную систему с помощью акторов, а тестирование сделать более надежным, используя формальную верификацию.
Цель работы: является проверка гипотезы путем реализации алгоритма Chord с помощью акторных систем и формальной верификации полученной реализации.
Объект исследования: методы уменьшения сложности разработки и тестирования распределенных систем
Предмет исследования: использование акторов и формальной верификации для уменьшения сложности разработки и тестирования в процессе имплементации алгоритма Chord
Метод или методология проведения работы: изучение основных понятий и методов формальной верификации, построения акторных систем, изучение и анализ разных версий алгоритма Chord, выбор реализуемых и верифицируемых черт алгоритма, поиск и выбор инструментов имплементации акторной системы и формальной верификации, имплементация и верификация алгоритма Chord с помощью этих инструментов.
Результаты работы: изучен и всесторонне проанализирован набор инструментов, подходящих для решения задачи, алгоритм Chord реализован с помощью акторных систем, полученная реализации формально верифицирована, сделаны некоторые выводы, касающиеся гипотезы.
Прогнозные предположения о развитии объекта исследования: продолжение поиска более новых эффективных комбинаций инструментов и внесении улучшений в кодовую базу существующих.