عنوان پایان‌نامه
مدل سازی و تحلیل اکتورها با قابلیت همه پخشی
- رشته تحصیلی
- مهندسی کامپیوتر -نرم افزار
- مقطع تحصیلی
- کارشناسی ارشد
- محل دفاع
- کتابخانه مرکزی پردیس 2 فنی شماره ثبت: E 3211;کتابخانه مرکزی -تالار اطلاع رسانی شماره ثبت: 81488;کتابخانه مرکزی پردیس 2 فنی شماره ثبت: E 3211;کتابخانه مرکزی -تالار اطلاع رسانی شماره ثبت: 81488
- تاریخ دفاع
- ۰۹ شهریور ۱۳۹۴
- دانشجو
- بهناز یوسفی
- استاد راهنما
- رامتین خسروی, فاطمه قاسمی اصفهانی
- چکیده
- ارتباطات همه‌پخشی به دلایل متفاوت ازجمله صرفه‌جویی در مصرف انرژی و افزایش بازدهی در بسیاری از سیستم‌های توزیع‌شده به کار گرفته می شود. با این وجود، مدل اکتور به عنوان مدلی برای سیستم‌های توزیع‌شده و همروند به طور مستقیم این‌گونه از ارتباطات را پشتیبانی نمی کند. در این موارد، یک ارتباط همه‌پخشی با چندین ارسال تک‌پخشی جایگزین می گردد که این امر موجب از دست رفتن هم‌پیمانگی و انفجار فضای‌حالت برای سیستم‌های نه‌چندان پیچیده می گردد. در اینجا، مدل ربکا، به عنوان یک مدل مبتنی بر اکتور، به منظور پشتیبانی از ارسال پیام‌های بینام و ناهمزمان به صورت همه‌پخشی گسترش می یابد، مدل گسترش‌یافته به اختصارbRebeca نامیده می شود. سپس به منظور کاهش فضای حالت روش کاهش شمارشی اعمال می گردد که از حل مسئله ی ساخت فضای حالت با در نظر گفتن حالت جهانی به صورت برداری از شمارنده ها، یکی برای هر حالت محلی غیر صفر، اجتناب می کند. این امر وارسی مدل را بدون در نظر گرفتن میحظات تقارنی ممکن می سازد. رویکرد ارائه شده برای سیستم‌های کامی متقارن مانند محیط های همه‌پخشی مناسب است. همچنین مدل اکتور با قابلیت همه‌پخشی چارچوب مناسبی جهت مدل‌سازی شبکه‌های حسگر بیسیم و شبکه‌های اقتضایی سیار فراهم می کند. با این تفاوت که در این شبکه‌ها، همه‌پخشی محدود به گره‌هایی است که در مجاورت فرستنده قرار دارند. اصطیحا به کانال شبکه بیسیم، کانال همه‌پخشی می گویند و به این ترتیب گره‌هایی که در همسایگی یکدیگر قرار دارند، اصطیحا متصل نامیده می شوند، مفهومی به نام همبندی را تعریف می کنند که به عنوان قسمتی از معنا مدل شده است. به دلیل سیار بودن گره‌ها، همبندی به صورت مداوم در حال تغییر می باشد. بنابراین، به منظور در نظر گرفتن کانال همه‌پخشی و تغییرات همبندی جهت وارسی مدل‌های شبکه‌های حسگر بیسیم و شبکه های سیار اقتضایی، مدل bRebeca در سطح معنایی گسترده می شود. سپس راهکار هایی جهت کاهش فضای حالت با/ بدون در نظر گرفتن قابلیت حرکت ارائه می شود. همچنین در رابطه با تاثیری که قابلیت حرکت بر اعمال روش کاهش انتزاع شمارشی می گذارد بحث می شود.
- Abstract
- Many distributed systems use broadcast communication for various reasons such as saving energy or increasing throughput. However, the actor model for concurrent and distributed systems does not directly support this kind of communication. In such cases, a broadcast must be modeled as multiple unicasts which leads to loss of modularity and state space explosion for any non-trivial system. Here, we extend Rebeca, an actor-based model language, to support asynchronous anonymous message broadcasting. Then, we apply counter abstraction for reducing the state space which efficiently by passes the constructive orbit problem by considering the global state as a vector of counters, one per each local state. This makes the model checking of systems possible without further consideration of symmetry. This approach is efficient for fully symmetric systems like broadcasting environments. The broadcasting actor model provides a suitable framework to model wireless sensor (WSNs) and mobile ad hoc networks (MANETs). In these networks, broadcast is restricted by locality of nodes, only those which are in the vicinity of the sender receive the sent message. Nodes which are in each other neighborhood considered connected. Connectivity of nodes defines the topology concept which is modeled as a part of semantics. Due to mobility of nodes, the underlying topology changes arbitrary. Therefore, to address local broadcast and topology changes, bRebeca is extended at the semantic level to allow verification of WSNs and MANETs. Then we propose some techniques to reduce the state space with and without mobility, and discuss how mobility effects the counter abstraction method. Finally, we use a couple of case studies to illustrate the applicability of our method and the way their state spaces are reduced in size. Keywords: state space reduction, broadcast, Rebeca, actor-based language, model checking, verification, MANETs.
