Верификация алгоритма забияки для распределенных систем средствами TLA+ и PlusCal
Аннотация
Данная работа посвящена верификации алгоритма забияки для распределенных систем средствами TLA+ и PlusCal. В работе обзорно приводится основная информация о распределенных системах, далее приводится краткая информация о распределенных алгоритмах выбора координатора, и, затем приводится подробный разбор распределенного алгоритма забияки на простом примере распределенной системы из семи узлов. Затем, в работе демонстрируется созданная модель распределенного алгоритма забияки на языках спецификации TLA+ и PlusCal и приводится описание основных частей данной модели. Далее приводится верификация созданной модели. Верификация производится при помощи инструмента TLC – это специализированное средство проверки моделей и симулятор для TLA+ спецификаций. Далее в работе продемонстрирован результат верификации. В результате верификации распределенного алгоритма забияки удалось установить, что заявленные свойства надежности и живучести выполняются в полной мере для всех возможных состояний системы.
Литература
2. Akhtar S., Zahoor E. Formal Specification and Verification of MQTT Protocol in PlusCal-2. Wireless Personal Communications. 2021; 119(2):1589-1606. (In Eng.) doi: https://doi.org/10.1007/s11277-021-08296-4
3. Shkarupylo V.V., Blinov I.V., Chemeris A.A., Dusheba V.V., Alsayaydeh J.A.J. On Applicability of Model Checking Technique in Power Systems and Electric Power Industry. In: Zaporozhets A. (ed). Systems, Decision and Control in Energy III. Studies in Systems, Decision and Control. Vol. 399. Springer, Cham; 2022. p. 3-21. (In Eng.) doi: https://doi.org/10.1007/978-3-030-87675-3_1
4. Akhtar S., Zahoor E., Perrin O. Formal Verification of Authorization Policies for Enterprise Social Networks Using PlusCal-2. In: Romdhani I., Shu L., Takahiro H., Zhou Z., Gordon T., Zeng D. (eds.). Collaborative Computing: Networking, Applications and Worksharing. CollaborateCom 2017. Lecture Notes of the Institute for Computer Sciences, Social Informatics and Telecommunications Engineering. Vol. 252. Springer, Cham; 2018. p. 530-540. (In Eng.) doi: https://doi.org/10.1007/978-3-030-00916-8_49
5. Resch S., Paulitsch M. Using TLA+ in the Development of a Safety-Critical Fault-Tolerant Middleware. 2017 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW). IEEE Press, Toulouse, France; 2017. p. 146-152. (In Eng.) doi: https://doi.org/10.1109/ISSREW.2017.43
6. Lamport L. The PlusCal Algorithm Language. In: Leucker M., Morgan C. (eds.). Theoretical Aspects of Computing ‒ ICTAC 2009. ICTAC 2009. Lecture Notes in Computer Science. Vol. 5684. Springer, Berlin, Heidelberg; 2009. p. 36-60. (In Eng.) doi: https://doi.org/10.1007/978-3-642-03466-4_2
7. Akhtar S., Merz S., Quinson M. A High-Level Language for Modeling Algorithms and Their Properties. In: Davies J., Silva L., Simao A. (eds.). Formal Methods: Foundations and Applications. SBMF 2010. Lecture Notes in Computer Science. Vol. 6527. Springer, Berlin, Heidelberg; 2011. p. 49-63. (In Eng.) doi: https://doi.org/10.1007/978-3-642-19829-8_4
8. Selvaratnam D., Cantoni M., Davoren J.M., Shames I. Sampling polynomial trajectories for LTL verification. Theoretical Computer Science. 2022; 897:135-163. (In Eng.) doi: https://doi.org/10.1016/j.tcs.2021.10.024
9. Rubio R., Martí-Oliet N., Pita I., Verdejo A. Model checking strategy-controlled systems in rewriting logic. Automated Software Engineering. 2022; 29(1). (In Eng.) doi: https://doi.org/10.1007/s10515-021-00307-9
10. Kovatsch M. CoAP for the web of things: From tiny resource-constrained devices to the web browser. Proceedings of the 2013 ACM Conference on Pervasive and Ubiquitous Computing Adjunct Publication. UbiComp’13 Adjunct. New York, NY: ACM; 2013. p. 1495-1504. (In Eng.) doi: https://doi.org/10.1145/2494091.2497583
11. Zahoor E., Ikram A., Akhtar S., Perrin O. Authorization Policies Specification and Consistency Management within Multi-cloud Environments. In: Gruschka N. (ed). Secure IT Systems. NordSec 2018. Lecture Notes in Computer Science. Vol. 11252. Springer, Cham; 2018. p. 272-288. (In Eng.) doi: https://doi.org/10.1007/978-3-030-03638-6_17
12. Kuppe M.A., Lamport L., Ricketts D. The TLA+ Toolbox. 5th Workshop on Formal Integrated Development Environment, F-IDE 2019. EPTCS 310. Porto, Portugal; 2019. p. 50-62. (In Eng.) doi: https://doi.org/10.4204/EPTCS.310.6
13. Shkarupylo V.V., Tomičić I., Kasian K.M. The investigation of TLC model checker properties. Journal of Information and Organizational Sciences. 2016; 40(1):145-152. (In Eng.) doi: https://doi.org/10.31341/jios.40.1.7
14. Park J.S., Sandhu R., Ahn G.-J. Role-based access control on the web. ACM Transactions on Information and System Security. 2001; 4(1):37-71. (In Eng.) doi: https://doi.org/10.1145/383775.383777
15. Yu Y., Manolios P., Lamport L. Model checking TLA+ specifications. In: Pierre L., Kropf T. (eds.). CHARME 1999. Lecture Notes in Networks and Systems. Vol. 1703. Springer, Heidelberg; 1999. p. 54-66. (In Eng.) doi: https://doi.org/10.1007/3-540-48153-2_6
16. Dutertre B., Easwaran A., Hall B., Steiner W. Model-based analysis of Timed-Triggered Ethernet. 2012 IEEE/AIAA 31st Digital Avionics Systems Conference (DASC). IEEE Press, Williamsburg, VA, USA; 2012. p. 9D2-1-9D2-11. (In Eng.) doi: https://doi.org/10.1109/DASC.2012.6382445
17. Bauer A., Leucker M., Schallhart C. Runtime Verification for LTL and TLTL. ACM Transactions on Software Engineering and Methodology. 2011; 20(4):14. (In Eng.) doi: https://doi.org/10.1145/2000799.2000800
18. Arghavani A., Ahmadi E., Haghighat A.T. Improved bully election algorithm in distributed systems. ICIMU 2011: Proceedings of the 5th international Conference on Information Technology & Multimedia. IEEE Press, Kuala Lumpur, Malaysia; 2011. p. 1-6. (In Eng.) doi: https://doi.org/10.1109/ICIMU.2011.6122724
19. Numan M., Subhan F., Khan W.Z., Assiri B., Armi N. Well-Organized Bully Leader Election Algorithm for Distributed System. 2018 International Conference on Radar, Antenna, Microwave, Electronics, and Telecommunications (ICRAMET). IEEE Press, Serpong, Indonesia; 2018. p. 5-10. (In Eng.) doi: https://doi.org/10.1109/ICRAMET.2018.8683916
20. Soundarabai P.B., Sahai R., Thriveni J., Venugopal K.R., Patnaik L.M. Improved Bully Election Algorithm for Distributed Systems. arXiv:1403.3255. 2014. Available at: https://arxiv.org/abs/1403.3255 (accessed 26.01.2022). (In Eng.)
21. Gholipour M., Kordafshari M.S., Jahanshahi M., Rahmani A.M. A New Approach for Election Algorithm in Distributed Systems. 2009 Second International Conference on Communication Theory, Reliability, and Quality of Service. IEEE Press, Colmar, France; 2009. p. 70-74. (In Eng.) doi: https://doi.org/10.1109/CTRQ.2009.32
22. Park S.H. A Probabilistically Correct Election Protocol in Asynchronous Distributed Systems. In: Zhou X., Xu M., Jähnichen S., Cao J. (eds.). Advanced Parallel Processing Technologies. APPT 2003. Lecture Notes in Computer Science. Vol. 2834. Springer, Berlin, Heidelberg; 2003. p. 177-185. (In Eng.) doi: https://doi.org/10.1007/978-3-540-39425-9_23
23. Dolev D. A simple model for agreement in distributed systems. In: Simons B., Spector A. (eds.). Fault-Tolerant Distributed Computing. Lecture Notes in Computer Science. Vol. 448. Springer, New York, NY; 1990. p. 42-50. (In Eng.) doi: https://doi.org/10.1007/BFb0042324
24. EffatParvar M., Yazdani N., EffatParvar M., Dadlani A., Khonsari A. Improved algorithms for leader election in distributed systems. 2010 2nd International Conference on Computer Engineering and Technology. IEEE Press, Chengdu, China; 2010. p. V2-6-V2-10. (In Eng.) doi: https://doi.org/10.1109/ICCET.2010.5485357
25. Johansson B., Rågberger M., Papadopoulos A.V., Nolte T. Heartbeat Bully: Failure Detection and Redundancy Role Selection for Network-Centric Controller. IECON 2020 The 46th Annual Conference of the IEEE Industrial Electronics Society. IEEE Press, Singapore; 2020. p. 2126-2133. (In Eng.) doi: https://doi.org/10.1109/IECON43393.2020.9254494
Это произведение доступно по лицензии Creative Commons «Attribution» («Атрибуция») 4.0 Всемирная.
Редакционная политика журнала основывается на традиционных этических принципах российской научной периодики и строится с учетом этических норм работы редакторов и издателей, закрепленных в Кодексе поведения и руководящих принципах наилучшей практики для редактора журнала (Code of Conduct and Best Practice Guidelines for Journal Editors) и Кодексе поведения для издателя журнала (Code of Conduct for Journal Publishers), разработанных Комитетом по публикационной этике - Committee on Publication Ethics (COPE). В процессе издательской деятельности редколлегия журнала руководствуется международными правилами охраны авторского права, нормами действующего законодательства РФ, международными издательскими стандартами и обязательной ссылке на первоисточник.
Журнал позволяет авторам сохранять авторское право без ограничений. Журнал позволяет авторам сохранить права на публикацию без ограничений.
Издательская политика в области авторского права и архивирования определяются «зеленым цветом» в базе данных SHERPA/RoMEO.
Все статьи распространяются на условиях лицензии Creative Commons «Attribution» («Атрибуция») 4.0 Всемирная, которая позволяет другим использовать, распространять, дополнять эту работу с обязательной ссылкой на оригинальную работу и публикацию в этом журналe.
