Lamport Algorithm Using Colored Petri Net with the Aim of Evaluating and Increasing Fault Tolerancy-Modeling Chandy
[Thesis]
/ابراهیم محمد البیاتی، علمدار
: Faculty of Computer Engineering
, 1398(2019)
, Mirzaei
69p.
Print - Electronic
M.A
, Faculty of Computer Engineering
1399/07/28
The distributed snapshot algorithm was discovered by Chandy-Lamport in 1985 and for its significance, studies are still ongoing until now. System snapshot in distributed system are used to solve many problems such as system recovery after a crash, determining system deadlock, distributed garbage collection, and determining whether the computation is terminated. One of the distributed system purposes is increasing fault tolerancy of the system. Inherent nature of distributed system causes that there will be no central point that captures a snapshot of whole system. Capturing processes' states of a distributed system at the same instant theoretically is impossible. The system components must work together to achieve snapshot. The asynchronous Chandy-Lamport distributed snapshot algorithm was modeled using a hierarchical color Petri net to achieve the study goal. The model consists of three layers, the first layer displays the system and its operations in general, the second layer shows the parts of operation for each process which are sending and receiving, and the third layer represents the core of what each process does in detail in terms of sending and receiving messages for the transfer of money or messages for the algorithm. The simulation of the designed system and state space calculation is performed to explore checking of the model for consistency among processes.
الگوریتم تصویر گیری توزیع شده توسط چاندی-لمپورت در سال 1985 کشف شد و برای اهمیت آن ، مطالعات هنوز هم ادامه دارد .تصویر گیری فوری سیستم در سیستم توزیع شده برای حل بسیاری از مشکلات مانند بازیابی سیستم پس از خرابی ، تعیین بن بست سیستم ، جمع آوری زباله توزیع شده و تعیین خاتمه محاسبات استفاده می شود .یکی از اهداف سیستم توزیع شده ، افزایش تحمل خطا در سیستم است .ماهیت ذاتی سیستم توزیع شده باعث می شود هیچ نقطه مرکزی وجود نداشته باشد که بتواند تصویری از کل سیستم را ثبت کند .گرفتن حالتهای فرآیندهای سیستم توزیع شده در همان لحظه از نظر تئوری غیرممکن است .اجزای سیستم برای دستیابی به تصویر گیری باید با هم کار کنند .الگوریتم تصویر گیری فوری توزیع شده غیر همزمان چاندی-لمپورت با استفاده از یک شبکه سلسله مراتبی پتری برای دستیابی به هدف مطالعه مدل سازی شد .این مدل از سه لایه تشکیل شده است ، لایه اول سیستم و عملکردهای آن را به طور کلی نمایش می دهد ، لایه دوم قسمت هایی از عملکرد را برای هر فرآیند ارسال و دریافت نشان می دهد و لایه سوم نشان دهنده هسته اصلی کار هر فرآیند از نظر ارسال و دریافت پیام برای انتقال پول یا پیام مخصوص الگوریتم است .شبیه سازی سیستم طراحی شده و محاسبه فضای حالت برای کشف بررسی مدل سازگاری بین فرآیندها انجام شده است
fa
مدل سازی الگوریتم چاندی-لمپورت با استفاده از شبکه پتری رنگی با هدف ارزیابی و افزایش میزان تحمل پذیری خرابی
Formal Method, Asynchronous Distributed System, Verification, Model Checking, Global State, Distributed Snapshot, Fault tolerancy
روش صوری ، سیستم توزیع غیر همزمان ، تأیید ، بررسی مدل ، حالت کلی ، تصویر گیری توزیع شده ، تحمل خطا