تطوير نموذج تجريدي لتوصيف خصائص الشبكات المتغيرة

نظراً للعدد الكبير من قواعد النفاذ المعرفة للشبكات والتغير الديناميكي لطوبولوجيا الشبكات, فان التحقق اليدوي من الخواص المهمة في الشبكة مثل الوصولية, عدم تضارب القواعد وعدم وجود حلقات امراً صعباً على المبرمج.يعدَ التوصيف الصوري(Formal Specification) للانظمة والبروتوكولات من اهم الطرق التي تستخدم لازالة الغموض في تعريفات الانظمة واكتشاف الثغرات في عملها.هناك العديد من الابحاث التي قدمت في مجال توصيف وصولية الرزم في الشبكات لكن القليل منها تم اختبارها عبر ادوات فحص النماذج التي تساعد في كشف اخطاء هذه النماذج.في هذا البحث تم تطوير نموذج تجريدي من اجل توصيف الشبكات الديناميكية ليصبح مناسباً للتحقق من مجموعة من الخصائص المهمة ومنها وصولية الرزم, عدم وجود التضاربات..الخ اعتماداً على ترميز حالة الشبكة. تم تحقيق النموذج المقترح الذي يوصف الشبكة بواسطة لغة المنطق الموقت للافعال(Temporal Logic of Action) ,TLA+ والتي هي عبارة عن لغة توصيف عالية المستوى, تعتمد على نظرية المجموعات والجبر المنطقي الاولي. تم تحليل النموذج وفحص خصائصه باستخدام اداة فحص النماذج TLCالمستخدمة مع الاداة TLA, تظهر النتائج صحة النموذج وتحسيناً من ناحية تخفيض زمن استجابة وعدد الحالات المطلوبة للحصول على نتيجة التحقق.