تعد عملية نقل الفيديو ضمن شبكات MANET مشكلة في غاية الأهمية نظراً إلى المتطّلبات الخاصة التي تحتاج إليها تطبيقات الوسائط المتعددة ( التأخير - جودة الخدمة ...) إِذ تتعرض الرزم للضياع و التأخير بسبب حركة العقد و تغير التوزع الجغرافي فضلاً عن التزاحم و سوء شروط القناة.
نظراً للعدد الكبير من قواعد النفاذ المعرفة للشبكات و التغير الديناميكي لطوبولوجيا الشبكات, فإن التحقق اليدوي من الخواص المهمة في الشبكة مثل الوصولية, عدم تضارب القواعد و عدم وجود حلقات أمراً صعباً على المبرمج.
يعدَ التوصيف الصوري (Formal Specificati
on) للأنظمة و البروتوكولات من أهم الطرق التي تستخدم لإزالة الغموض في تعريفات الأنظمة و اكتشاف الثغرات في عملها.
هناك العديد من الأبحاث التي قدمت في مجال توصيف وصولية الرزم في الشبكات لكن القليل منها تم اختبارها عبر أدوات فحص النماذج التي تساعد في كشف أخطاء هذه النماذج.
في هذا البحث تم تطوير نموذج تجريدي من أجل توصيف الشبكات الديناميكية ليصبح مناسباً للتحقق من مجموعة من الخصائص المهمة و منها وصولية الرزم, عدم وجود التضاربات..الخ اعتماداً على ترميز حالة الشبكة. تم تحقيق النموذج المقترح الذي يوصف الشبكة بواسطة لغة المنطق المؤقت للأفعال (Temporal Logic of Action) ,TLA+ و التي هي عبارة عن لغة توصيف عالية المستوى, تعتمد على نظرية المجموعات و الجبر المنطقي الأولي. تم تحليل النموذج و فحص خصائصه باستخدام أداة فحص النماذج TLC المستخدمة مع الأداة TLA, تظهر النتائج صحة النموذج و تحسيناً من ناحية تخفيض زمن استجابة و عدد الحالات المطلوبة للحصول على نتيجة التحقق.
في هذا البحث تم توصيف الشبكة بواسط الجبر المنطقي و ذلك لكي يتم فرز الرزم إلى
مجموعتين تتضمن الرزم التي ستصل إلى الهدف و الرزم التي سيتم سحبها وفق حالة
الشبكة و جداول التدفق, تم كتاب التوصيف باستخدام لغة TLA+ التي تعتمد على الجبر
المنطقي الأولي و
تم فحص النموذج بواسطة أداة TLCحيث تساعد هذه الطريقه على
عملية التحقق المسبق (Proactive verification) لتعريفات الشبكة و التأكد من أنها
تتعارض مع السياسة الأمنيه العامه.
تم تشييد سد الصوراني لتأمين مياه الشرب للقرى السكنية الواقعة في منطقة الشيخ بدر - محافظة طرطوس, لكن مياه بحيرة السد تتعرض لملوثات من مصادر متعددة مما حال دون استخدامها لأغراض الشرب. نسعى في هذا البحث لمناقشة الآلية التي يتم وفقها التلوث و اقتراح الإج
راءات المناسبة للحد منه، من خلال دراسة بعض التغيرات الفيزيائية و الكيميائية و البيولوجية للمياه في مواقع مختلفة من بحيرة سد الصوراني و الروافد المغذية لها.
أظهرت نتائج الدراسة ارتفاع قيم العكارة و الأس الهيدروجيني في فصلي الخريف و الشتاء و ذلك في مياه الروافد مقارنة بمياه البحيرة، و يعود ذلك إلى نشاط الجريان بفعل الهطول المطري في تلك الفترة. في حين أن شاردة الأمونيوم أبدت ارتفاعاً ملحوظاً في موقع ذيل البحيرة، و يمكن أن يعزى ذلك إلى إلقاء مخلفات الصرف الصحي الناتجة عن قرية برمانة المشايخ مباشرة في المياه الواردة إلى البحيرة. كما تبيّن وجود تغيرات فصلية كبيرة في التعداد الكلي للأحياء الدقيقة ضمن جميع المواقع المدروسة، و كان أعلاها في رافد عين الزعرور خلال الشتاء إذ وصلت إلى 5.36 × 104خلية /100مل. خلصت الدراسة إلى أن المصدر الرئيسي لتلوث مياه البحيرة هو المياه الملوثة الواردة اليها من قرية برمانة المشايخ، إضافة إلى رافد عين الزعرور المار بالقرب من منشآت سياحية لقرية الصوراني، يليه رافد الوادي الأخضر الذي يغذي مياه البحيرة في جميع فصول السنة. مصادر التلوث هذه تجعل مياه البحيرة غير صالحة للشرب و ينبغي تعقيمها قبل استخدامها لهذا الغرض.
نقدم في هذا البحث نموذجاً صورياً لتوصيف عملية هجرة المضيفات في SDN بحيث
يتم التأكد من خاصية الوصولية (Reachability ) لمرزم و عدم تغييرها بعد الانتقال
و تحقيق التعديلات المطلوبة لكي يتم الحفاظ على نفس الخصائص. تم تصميم النموذج
بواسطة لغة التوصيف
الصوري TLA+ و التحقق منه من خلال أداة فحص النماذج TLC
المترافقة معه, حيث تميز النموذج بعدد قليل للحالات لتحقيق المطلوب.
