Распределенные алгоритмы и их верификация с помощью Byzantine model checker

Вестник КазНУ. Серия математика, механика, информатика

A. T. Bektemessov¹  F. A. Iliyaletdinov¹  A. Zh. Burlibaev¹ 

[1] Казахский национальный университет имени аль-Фараби;

关键词: распределенные алгоритмы;    параллельная программа;    bymc;    model checking;    верификация;   

DOI  :  

来源: DOAJ

【 摘 要 】

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

【 授权许可】

Unknown