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

Authors

  • رضوان دندة
  • قاسم قبلان
  • سوسن يوسف

Abstract

نظراً للعدد الكبير من قواعد النفاذ المعرفة للشبكات والتغير الديناميكي لطوبولوجيا الشبكات, فإن التحقق اليدوي من الخواص المهمة في الشبكة مثل الوصولية, عدم تضارب القواعد وعدم وجود حلقات أمراً صعباً على المبرمج. يعدَ التوصيف الصوري(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.

Downloads

Published

2017-10-24

How to Cite

1.
دندة ر, قبلان ق, يوسف س. تطوير نموذج تجريدي لتوصيف خصائص الشبكات المتغيرة. Tuj-eng [Internet]. 2017Oct.24 [cited 2025Apr.21];38(5). Available from: https://journal.tishreen.edu.sy/index.php/engscnc/article/view/3257

Issue

Vol. 38 No. 5 (2016): العلوم الهندسية

Section

Articles

License

Copyright (c) 2017 �ttps://creativecommons.org/licenses/by-nc-sa/4.0/

Creative Commons License

This work is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License.

The authors retain the copyright and grant the right to publish in the magazine for the first time with the transfer of the commercial right to Tishreen University Journal for Research and Scientific Studies - Engineering Sciences Series

 Under a CC BY- NC-SA 04 license that allows others to share the work with of the work's authorship and initial publication in this journal. Authors can use a copy of their articles in their scientific activity, and on their scientific websites, provided that the place of publication is indicted in  Tishreen University Journal for Research and Scientific Studies - Engineering Sciences Series   .  The Readers have the right to send, print and subscribe to the initial version of the article, and the title of  Tishreen University Journal for Research and Scientific Studies - Engineering Sciences Series     Publisher

journal uses a CC BY-NC-SA license which mean

You are free to:

  • Adapt — remix, transform, and build upon the material
  •  
  • The licensor cannot revoke these freedoms as long as you follow the license terms.

 

  • Attribution — You must give appropriate credit, provide a link to the license, and indicate if changes were made. You may do so in any reasonable manner, but not in any way that suggests the licensor endorses you or your use.
  • NonCommercial — You may not use the material for commercial purposes.
  • ShareAlike — If you remix, transform, or build upon the material, you must distribute your contributions under the same license as the original.
  • No additional restrictions — You may not apply legal terms or technological measures that legally restrict others from doing anything the license permits.

Most read articles by the same author(s)

1 2 > >>