في هذا البحث تم توصيف الشبكة بواسط الجبر المنطقي و ذلك لكي يتم فرز الرزم إلى
مجموعتين تتضمن الرزم التي ستصل إلى الهدف و الرزم التي سيتم سحبها وفق حالة
الشبكة و جداول التدفق, تم كتاب التوصيف باستخدام لغة TLA+ التي تعتمد على الجبر
المنطقي الأولي و
تم فحص النموذج بواسطة أداة TLCحيث تساعد هذه الطريقه على
عملية التحقق المسبق (Proactive verification) لتعريفات الشبكة و التأكد من أنها
تتعارض مع السياسة الأمنيه العامه.
نقدم في هذا البحث نموذجاً صورياً لتوصيف عملية هجرة المضيفات في SDN بحيث
يتم التأكد من خاصية الوصولية (Reachability ) لمرزم و عدم تغييرها بعد الانتقال
و تحقيق التعديلات المطلوبة لكي يتم الحفاظ على نفس الخصائص. تم تصميم النموذج
بواسطة لغة التوصيف
الصوري TLA+ و التحقق منه من خلال أداة فحص النماذج TLC
المترافقة معه, حيث تميز النموذج بعدد قليل للحالات لتحقيق المطلوب.