اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدتطوير نموذج تجريدي لتوصيف خصائص الشبكات المتغيرة
A development of an abstraction model for specifying dynamic networks properties
852
0 24
0
(
0
)
نشر من قبل
جامعة تشرين ورقة بحثية
تاريخ النشر
2016
مجال البحث
الهندسة المعلوماتية
والبحث باللغة
العربية
تمت اﻹضافة من قبل
Shamra Editor
اسأل ChatGPT حول البحث
نظراً للعدد الكبير من قواعد النفاذ المعرفة للشبكات و التغير الديناميكي لطوبولوجيا الشبكات, فإن التحقق اليدوي من الخواص المهمة في الشبكة مثل الوصولية, عدم تضارب القواعد و عدم وجود حلقات أمراً صعباً على المبرمج. يعدَ التوصيف الصوري (Formal Specification) للأنظمة و البروتوكولات من أهم الطرق التي تستخدم لإزالة الغموض في تعريفات الأنظمة و اكتشاف الثغرات في عملها. هناك العديد من الأبحاث التي قدمت في مجال توصيف وصولية الرزم في الشبكات لكن القليل منها تم اختبارها عبر أدوات فحص النماذج التي تساعد في كشف أخطاء هذه النماذج. في هذا البحث تم تطوير نموذج تجريدي من أجل توصيف الشبكات الديناميكية ليصبح مناسباً للتحقق من مجموعة من الخصائص المهمة و منها وصولية الرزم, عدم وجود التضاربات..الخ اعتماداً على ترميز حالة الشبكة. تم تحقيق النموذج المقترح الذي يوصف الشبكة بواسطة لغة المنطق المؤقت للأفعال (Temporal Logic of Action) ,TLA+ و التي هي عبارة عن لغة توصيف عالية المستوى, تعتمد على نظرية المجموعات و الجبر المنطقي الأولي. تم تحليل النموذج و فحص خصائصه باستخدام أداة فحص النماذج TLC المستخدمة مع الأداة TLA, تظهر النتائج صحة النموذج و تحسيناً من ناحية تخفيض زمن استجابة و عدد الحالات المطلوبة للحصول على نتيجة التحقق.
According to the large number of the access rules that define the networks, and the dynamic changing of the network topology, that is the verification by hand of the important properties in the network such as reachability, access rules conflict free and loop free is so hard to accomplish by the programmer. Formal specification of systems and protocols is considered one of the most important methods that is used to eliminate the ambiguous of the system configurations and find bugs of its work. A lot of the researches have been introduced in packet reachability and network specification domain, but a little of them are checked and analyzed by model checkers which help to detect the errors of these models. In this paper an abstraction model for dynamic networks specification has been introduced and developed to be appropriate for several important properties of the network such as reachability, no conflict..etc, depending on the network state. The proposed model specification is implemented by TLA+(Temporal Logic of Action) language which is a high level specification language built on Set-theory and First Order Logic, the model has been analyzed and the properties are checked by TLC model checking tool which used by TLA tool. Results show the correctness of the model, and improvement in reducing the response time and the required states to get the result of the verification.
المراجع المستخدمة
LAMSWEERDE,A.V., Formal specification.The conference on the future of Software engineering – USA,2000,147-159
GUTTMAN., Filtering postures: Local enforcement for global policies".IEEE,1997,60-67
JEFFREY,A., SAMAK,T., Model checking firewall policy configurations. In: IEEE International Workshop on Policies for Distributed Systems and Networks, 2009, 60–67
قيم البحث
اقرأ أيضاً
تعاني الشبكات الخليوية من مشكلة تقديم خدمة بجودة عالية لكافة المستخدمين نظراً للضغط الكبير عليها، و مع تزايد عدد المستخدمين يتزايد الطلب على الانترنت عن طريق الخليوي خصوصاً بعد التطور التكنولوجي الكبير الذي يشهده عصرنا الحالي. بانتقال المستخدم بين م
نزله و مكان عمله يحتاج إلى شبكة تؤمن له اتصالاً بمستوى جودة مقبول على الأقل و بأقل احتمال ممكن لانقطاع اتصاله. تقدم الشبكات الخليوية المعتمدة على بروتوكول الانترنت Cellular IP Networks حلاً جيداً لكونها تدعم المستخدمين ذوي قابلية التحرك الكبيرة، لكن مع ازدياد حاجة المستخدمين و تنوعها (تحميل ملفات، مشاهدة فيديو، إرسال بريد الكتروني...) تظهر الحاجة إلى إيجاد طرق فعالة لتحسين جودة الخدمة المقدمة في هذه الشبكات.
يعتبر عرض الحزمة من أهم العوامل المؤثرة في جودة الخدمة، لذا نقترح في هذا البحث طريقة لإدارة عرض حزمة الشبكة الخليوية المعتمدة على بروتوكول الانترنت عن طريق استعارة جزء من عرض الحزمة المقدم للمستخدمين في الزمن غير الحقيقي باستخدام خوارزمية الأسراب، و الحفاظ على عرض حزمة معين في الاتصالات الجارية في الزمن غير الحقيقي ضمن الخلية الهدف، و الذي يشكل عتبة أمان لهذه الاتصالات بحيث لا ينخفض عرض الحزمة المخصص لها إلى أقل من هذه العتبة مما يحميها من الانقطاع.
يرتكز البحث على نمذجة عملية التسليم و تطبيق النموذج المقترح للوصول إلى أفضل نتيجة تؤمن أقل نسبة قطع لعملية التسليم و أقل نسبة لحجبها.
هدف هذا البحث إلى تطوير نموذج مساعد على اتخاذ القرار بشأن إستراتيجية الصيانة المثلى للمعدات المستخدمة في تنفيذ مشروعات التشييد، و نقصد بالصيانة المثلى تلك المحققة للكلفة الدنيا. حيث تبرز الحاجة لوجود نظام يتم من خلاله التحكم بخطة عمل و صيانة الآليات
بما يضمن حدوث أقل توقفات ممكنة، و ذلك من خلال وجود برنامج لصيانة مختلف الأعطال و إصلاحها آخذين بالحسبان تحقيق أقل كلفة ممكنة (سواء كانت كلفة الإصلاح أو الخسائر الناتجة عن توقفات العمل المتعلقة بالصيانة) بحيث يسهم ذلك في النهاية في تخفيض الكلفة النهائية للمشروع.
في هذا البحث تم إجراء تعديلات على TCP بإدخال تأخير متكيف و مستجيب للضياعات adaptive delay and loss (TCP-ADaLR) response للتقليل من حدة الآثار السلبية لخصائص الأقمار الصناعية.
يقدم هذا البحث نموذجاً رياضياً دقيقاً لمحرك تحريضي ثلاثي الطور من
أجل دراسته في الحالات العابرة و الدائمة (المستقرة) على حد سواء. يأخذ هذا
النموذج بعين الإعتبار: توافقيات منبع التغذية - أثر القشرة - الإشباع المغناطيسي
في الثابت و الدوار. الأمر الذ
ي يمكنه من تمثيل المحرك الحقيقي و ظواهره الفيزيائية
الداخلية بشكل أفضل من النماذج التقليدية الموجودة.
يبين المشروع كيفية تصميم نموذج باستخدام أدوات التحليل المكاني (spatial Analysis) المتاحة في برامج نظم المعلومات الجغرافية لاختيار أفضل المواقع لإنشاء منشأة سياحية في محافظة طرطوس, ثم قمنا بتخصيص معاملات إدخال للنموذج لكي يتم تطبيقه على مناطق مختلفة ب
استخدام بيانات إدخال مختلفة ليتمكن مستخدمو النموذج ببساطة من إدخال المعاملات الخاصة بهم في منطقتهم دون الحاجة إلى معرفة كثير من المعلومات حول واقع عمل النموذج، وتكمن أهمية المشروع من خلال تقديم نموذج كامل باستخدام باني النماذج (ModelBuilder) ضمن برنامج ArcGIS لاختيار أفضل موقع لمنشأة سياحية تحقق مجموعة من المعايير، وتقديم واجهة مستخدم لوضع البيانات الضرورية مباشرة, وسيتم تحقيق هذه الأهمية من خلال مجموعة من الأهداف نستعرضها فيما يلي :
• دراسة نظرية لنظم المعلومات الجغرافية (GIS) والتحليل المكاني حيث سنعرض مقدمة تبين أهمية برنامج ArcGIS وأدوات التحليل المكاني المتوفرة ضمن بيئة نظم المعلومات الجغرافية والتي اعتمدنا عليها لإنشاء النموذج المطلوب.
• دراسة نظرية لباني النماذج (ModelBuilder) ضمن برنامج ArcGIS، ثم سنستعرض فوائد النموذج وضبط إعداداته وبنائه بخطوات متكاملة.
• تطبيق منهجية التحليل المكاني باستخدام GIS)) وبناء نموذج لاختيار أفضل موقع لمنشأة سياحية تحقق مجموعة من المعايير في منطقة الدراسة، ذلك بالاعتماد على البيانات المتوفرة واشتقاق بيانات جديدة تساهم في إتمام عملية بناء النموذج، وتحديد المعاملات اللازمة التي ستظهر في واجهة المستخدم المطلوبة لاختيار الموقع الأفضل.
الأسئلة المقترحة
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
