توصيف عملية هجرة المضيفات في الشبكات المعرفة بالبرمجة SDN
نشر في جامعة البعث
بتاريخ 2016
في مجال
والبحث باللغة
العربية
تحميل البحث
الملخص بالعربية
نقدم في هذا البحث نموذجاً صورياً لتوصيف عملية هجرة المضيفات في SDN بحيث
يتم التأكد من خاصية الوصولية (Reachability ) لمرزم و عدم تغييرها بعد الانتقال
و تحقيق التعديلات المطلوبة لكي يتم الحفاظ على نفس الخصائص. تم تصميم النموذج
بواسطة لغة التوصيف الصوري TLA+ و التحقق منه من خلال أداة فحص النماذج TLC
المترافقة معه, حيث تميز النموذج بعدد قليل للحالات لتحقيق المطلوب.
المراجع المستخدمة
AL-SHAER,E., MARRERO,W., EL-ATAWY,E., ELBADAWI,K., 2009- Network configuration in a box: towards end-to-end verification of network reachability and security. ICNP-17th IEEE International Conference , PP:123– 132
CHURCHED, A, ZHOU, W, CAESAR, M. &GODFREY,P., 2012- “Overflow: Verifying network-wide invariants in real time,” ACM SIGCOMM Computer Communication Review, vol. 42, no. 4, PP:467–472
HP business white paper, 2013- prepare for software defined networking , build the foundation for SDN with OpenFlow. URL: hp.com/networking/openflow