دانلود ترجمه مقاله آنالیز پروتکل PGM به وسیله مدل اوپال

• بخشی از ترجمه:

چکیده ترجمه:
پروتکل چندبخشی عمومی عملگرا (PGM) به عنوان یه پروتکل چندبخشی معتبری می باشد که به منظور به حداقل رساندن احتمالات انفجار تایید منفی (NAK) و ظرفیت شبکه شبکه به دلیل ارسال مجدد بسته های از دست رفته، طراحی می شود. این پروتکل برای کارگروه مهندسی اینترنتی به عنوان یک معیار منبع باز ارائه شده است.
در این مقاله، تمرکزمان را بر روی ویژگی های قابل اطمینانی مهمی قرار می دهیم که پروتکل چندبخشی عمومی عملگرا (PGM) به تضمین آن می پردازد. گیرنده تمام بسته های داده را از موارد ارسالی دریافت کرده و آن ها را اصلاح می کند یا قادر به آشکارسازی بسته های داده از بین رفته غیر قابل بازیابی می باشد.
ما در ابتدا مدل ( نسخه ساده ای) از پروتکل چندبخشی عمومی عملگرا (PGM) را از طریق شبکه اتوماسیون زمان مطرح می کنیم. سپس با استفاده از بررسی کننده مدل UPPAAL، به بررسی صحت ویژگی های قابل اطمینان بالا می پردازیم، که همیشه محقق نبوده، اما بستگی به مقادیر چندین پارامتر که مد نظر قرار می دهیم، دارد.
١. مقدمه
از زمان معرقی فرایندهای اتوماتیک زمانی، فعالیت های زیادی به بررسی های نظری مدل های زمانی و موضوعات عملی برای تجزیه تحلیل آن ها اختصاص داده شده است. الگوریتم های اثباتی طراحی شده و در ارزیاب مدل های زمانی واقعی همانند های تک، کرونوس، یا UPPAAL به اجرا در آمده اند، که نتایج موفقی را برای بررسی های موردی مختلف داشته اند. در این مقاله ما به اثبات دو ویژگی قابل اطمینان برای پروتکل قابل اطمینان پروتکل چندبخشی عمومی عملگرا (PGM) می پردازیم.

• بخشی از مقاله انگلیسی:

Abstract

Pragmatic General Multicast (PGM) is a reliable multicast protocol, designed to minimize both the probability of negative acknowledgements (NAK) implosion and the load of the network due to retransmissions of lost packets. This protocol was presented to the Internet Engineering Task Force as an open reference specification. In this paper, we focus on the main reliability property which PGM intends to guarantee: a receiver either receives all data packets from transmissions and repairs or is able to detect unrecoverable data packet loss. We first propose a modelization of (a simplified version of) PGM via a network of timed automata. Using Uppaal model-checker, we then study the validity of the reliability property above, which turns out not to be always verified but to depend on the values of several parameters that we underscore. 1 Introduction Since the introduction of timed automata (Alur and Dill (1990)), a lot of work has been devoted to both theoretical studies of timed models and practical issues for their analysis. Verification algorithms have been designed and implemented in so-called real-time model-checkers like HyTech (Henzinger et al. (1997)), Kronos (Bozga et al. (1998)) or Uppaal (Larsen et al. (1997)), with successful results for numerous case studies. In this paper, we propose the verification of two reliability properties for the multicast protocol PGM. Reliable multicast protocols. Reliable multicast protocols are designed to enable distribution of information from multiple sources to multiple receivers, with reliability requirements. Examples of applications which may benefit from this technology include video broadcasts, data base replication or software downloads. Reliability in unicast protocols (like TCP) is usually achieved by positive acknowledgments (ACK) sent by the receiver to the source. Extending this principle to multicast protocols with a growing number of receivers may result in so-called ACK implosion. For this reason, the development of multicast protocols initially focused on eliminating ACKs, while keeping negative acknowledgements (NAK), invoked by receivers only when some packets are not received. However, multiple redundant NAKs can also be issued if packets are

دانلود رایگان مقاله انگلیسی

خرید ترجمه فارسی مقاله