Распределенные алгоритмы и их верификация с помощью Byzantine model checker
Ключевые слова:
распределенные алгоритмы, параллельная программа, ByMC, model checking, верификацияАннотация
Каждый алгоритм системы является главным узлом для построения надежных распределенных систем. Для того, чтобы быть уверенным в том, что эти алгоритмы делают систему более надежной, мы должны гарантировать, что предлагаемые алгоритмы работают правильно. Однако, проверка на модели внедренной отказоустойчивости распределенных алгоритмов [1] в действительности возможно использовать только для очень маленьких систем, чтобы в конечном итоге иметь возможность автоматически проверять отказоустойчивость распределенных алгоритмов на больших системах. В этой статье мы рассмотрим моделирование и проверку алгоритма "Parsing"методом Broadcast вещания [2] с помощью Spin и ByMC (Byzantine Model Checker [3]). Предлагаемые свойства обеспечивают безопасность и живучесть на LTL (Linear-temporal logic).
