کامپیوتر 23. تجزیه و تحلیل پروتکل PGM توسط UPPAAL

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