Распределенные алгоритмы и их верификация с помощью Byzantine model checker
Кілттік сөздер:
распределенные алгоритмы, параллельная программа, ByMC, model checking, верификацияАннотация
Каждый алгоритм системы является главным узлом для построения надежных распределенных систем. Для того, чтобы быть уверенным в том, что эти алгоритмы делают систему более надежной, мы должны гарантировать, что предлагаемые алгоритмы работают правильно. Однако, проверка на модели внедренной отказоустойчивости распределенных алгоритмов [1] в действительности возможно использовать только для очень маленьких систем, чтобы в конечном итоге иметь возможность автоматически проверять отказоустойчивость распределенных алгоритмов на больших системах. В этой статье мы рассмотрим моделирование и проверку алгоритма "Parsing"методом Broadcast вещания [2] с помощью Spin и ByMC (Byzantine Model Checker [3]). Предлагаемые свойства обеспечивают безопасность и живучесть на LTL (Linear-temporal logic).
Библиографиялық сілтемелер
[2] Srikanth T., Toueg S. Simulating authenticated broadcasts to derive simple fault-tolerant algorithms. // Distributed Computing 2, - 1987. - P. 80–94.
[3] John A., Konnov I., Schmid U., Veith H., Widder J. Counter Attack on Byzantine Generals: Parameterized Model Checking of Fault-tolerant Distributed Algorithms. // Cornell University Library. Ithaca. NY. - V2. - 2013. - P. 56-75.
[4] Miner D., Shook A. MapReduce Design Patterns. Building Effective Algorithms and Analytics for Hadoop and Other Systems. // Ottawa. Canada. ACM. NY. - 2012. – P. 204–213.
[5] Akhmed-Zaki D.Zh., Bektemessov A.T. Simulation of distributed programm with transactional memory. // Buletin KazNU. Almaty – 2014. – P. 26-33.
[6] Charron-Bost B., Pedone F., Schiper A. Replication: Theory and Practice // Lecture Notes in Computer Science. Springer. - V 5959. - 2010. - P. 156-167.
[7] Bokor P., Kinder J., Serafini M., Suri N. Efficient model checking of fault-tolerant distributed protocols. // In: DSN. - 2011. - P. 73–84.
[8] Clarke E. M., Grumberg O., Peled D.A. Model Checking // The MIT Press. London. England. - 1999. –330 p.
[9] John A., Konnov I., Schmid U., Veith H., Widder J. Starting a dialog between model checking and fault-tolerant distributed algorithms // arXiv CoRR abs/1210.3839. - 2012.
[10] Aubakirov S., Trigo P. and Ahmed-Zaki D. Comparison of Distributed Computing Approaches to Complexity of n-gram Extraction // Agent and Systems Modeling, Portugal Proceedings of DATA, - 2016. –P. 25–30.
[11] Clarke E., Grumberg O., Jha S., Lu Y., Veith H. Counterexample-guided abstraction refinement for symbolic model checking. // J.ACM 50(5). - 2003. - P. 752–794
[12] Benchmarks Spin2013 ByMC 0.9.5: Byzantine model checker, http://forsyte.tuwien.ac.at/software/bymc/ (Application date: 05.08.2016)
