عنوان پایان‌نامه
وارسی مدل های شبکه های اقتضایی با استفاده از قیود شبکه
- رشته تحصیلی
- مهندسی کامپیوتر -نرم افزار
- مقطع تحصیلی
- کارشناسی ارشد
- محل دفاع
- کتابخانه مرکزی پردیس 2 فنی شماره ثبت: E 2777;کتابخانه مرکزی -تالار اطلاع رسانی شماره ثبت: 70207
- تاریخ دفاع
- ۲۰ شهریور ۱۳۹۳
- دانشجو
- سعیده احمدی
- استاد راهنما
- فاطمه قاسمی اصفهانی
- چکیده
- شبکه‌های سیار اقتضایی شبکه‌هایی غیر متمرکز هستند که در آن‌ها گره‌ها دارای زیرساخت ثابتی نیستند. این گره‌ها یا به طور مستقیم و به کمک فرستنده‌ها و گیرنده‌های بی‌سیم یا به طور غیر مستقیم و به واسطه سایر گره‌ها با هم ارتباط برقرار می‌کنند. گره‌ها می‌توانند سیار باشند که این امر منجر به پویایی همبندی شبکه می‌گردد. پویایی همبندی، طراحی قراردادهای این شبکه‌ها را به چالش کشیده است. لازم است که قراردادها طوری طراحی گردند که نسبت به تغییرات ناگهانی همبندی مصون باشند. به طور معمول، قراردادها به وسیله‌ی شبیه‌سازی و آزمون درستی‌یابی می‌شوند؛ اما عدم یافتن خطا در آزمون و شبیه‌سازی به معنی عدم وجود اشتباه نیست. بنابراین در مقابل این‌گونه روش‌ها، روش‌های صوری که نسبت به روش های مذکور می‌توانند ابهام کمتر و دقت بیان بیشتری داشته باشند به عنوان یک چاچوب ریاضی استفاده می‌شوند. در این پایان‌نامه، چارچوب ریاضی جبر فرآیندی همه‌پخشی محلی که به جهت توصیف و ارزیابی شبکه‌های سیار اقتضایی ارائه گردیده است، را تغییر می‌دهیم تا به جای ارتباطات بااتلاف، بتوان خطا‌های ناشی از اشکال و نقص قرارداد را تشخیص داد. همچنین، به منظور ارزیابی قراردادهای شبکه سیار اقتضایی، یک منطق زمانی درخت محاسباتی به نام منطق درخت محاسباتی مبتنی بر کُنش مقید (CACTL) ارائه می‌دهیم که بر روی سیستم گذار برچسب‌دار مقید تفسیر می‌گردد. عملگر‌های زمانی این منطق با قیود چند‌پرشی روی همبندی‌های شبکه پارامتر‌دهی می‌شود تا به هنگام تحلیل رفتار یک قرارداد، علاوه بر رفتار قراردادها در طول زمان، اطلاعات همبندی نیز مدنظر قرار گرفته شود. وارسی‌گر الگو منطق توصیف خصایص CACTL را با استفاده از زبان ماد پیاده‌سازی می‌کنیم. در نهایت، کاربردپذیری منطق توصیف خصایص ارائه شده برای وارسی الگو قراردادهای شبکه‌های سیار اقتضایی را در قالب یک نمونه مطالعه موردی نشان می‌دهیم.
- Abstract
- Mobile Ad hoc Networks are decentralized networks, without any static infrastructure . In these networks, nodes communicate directly or indirectly via other nodes. They could move arbitrary, which makes the underlying topology dynamic. Node mobility complicates the design of this network protocols. The protocols need to be designed protected against arbitrary mobility. Usually, protocols are verified by testing or simulation; but, in these methods, finding no error does not mean that there is no fault. In contrast to these methods, formal methods that can be less ambiguous and more accurate are used as a mathematical framework. In this thesis, we modify Restricted Broadcast Process Theory, which has been introduced for specification and verification of mobile ad hoc networks, to detect faults resulting from protocol malfunction rather than lossy communication. Moreover, for model checking the Mobile Ad hoc Network protocols, we introduce a branching-time temporal logic named Constrained Action Computation Tree Logic (CACTL) which is interpreted over the constrained labeled transition systems. The temporal operators of this Logic are parameterized by multi-hop constraints over topologies so that for analyzing the protocol behaviors in addition to temporal behaviors, topological information are considered too. We implement a model checker for CACTL, using the rewriting logic of Maude. Finally, we represent the efficacy of presented property specification logic for model checking of Mobile Ad hoc Network protocols by a case-study.
