نشر في جامعة البعث
بتاريخ 2016
في مجال
والبحث باللغة
العربية
تحميل البحث
الملخص بالعربية
في هذا البحث تم توصيف الشبكة بواسط الجبر المنطقي و ذلك لكي يتم فرز الرزم إلى
مجموعتين تتضمن الرزم التي ستصل إلى الهدف و الرزم التي سيتم سحبها وفق حالة
الشبكة و جداول التدفق, تم كتاب التوصيف باستخدام لغة TLA+ التي تعتمد على الجبر
المنطقي الأولي و تم فحص النموذج بواسطة أداة TLCحيث تساعد هذه الطريقه على
عملية التحقق المسبق (Proactive verification) لتعريفات الشبكة و التأكد من أنها
تتعارض مع السياسة الأمنيه العامه.
المراجع المستخدمة
AL-SHAER, E, & AL-HAJ, S, 2010 - FlowChecker: Configuration Analysis and Verification of Federated OpenFlow Infrastructures. In Proceedings of the 3rd ACM Workshop on Assurable and Usable Security Configuration,ACM PP: 37–44
BALL, T, & BJØRNER, N, & GEMBER, A, & ITZHAKY, S, 2014 - VeriCon: Towards Verifying Controller Programs in Software-Defined Networks. ACM, PP. 1-12
BAIER, C, & KATOEN, J 2007 - Principles of Model Checking. The MIT Press Cambridge, Massachusetts, England, May. (992)P