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