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