ترغب بنشر مسار تعليمي؟ اضغط هنا

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

هل ترغب بارسال اشعارات عن اخر التحديثات في شمرا-اكاديميا