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