عنوان پایان‌نامه
مدل سازی و تحلیل اکتورهای زمان دار مبتنی بر منطق بازنویسی
- رشته تحصیلی
- مهندسی کامپیوتر -نرم افزار
- مقطع تحصیلی
- کارشناسی ارشد
- محل دفاع
- کتابخانه مرکزی پردیس 2 فنی شماره ثبت: E 2486;کتابخانه مرکزی -تالار اطلاع رسانی شماره ثبت: 63925
- تاریخ دفاع
- ۱۳ شهریور ۱۳۹۲
- دانشجو
- زینب صباحی کاویانی
- استاد راهنما
- رامتین خسروی
- چکیده
- مدل اکتور، یک مدل کارآمد برای توصیف محاسبات ناهمگام و توزیع‌شده است و در صورت وجود قیود زمانی در سیستم، مدل اکتور زمان‌دار مطرح می‌گردد. برای تحلیل سیستم‌ها بر طبق این مدل، می‌بایست از زبان‌های موجود مبتنی بر اکتور زمان‌دار استفاده کرد. چندین زبان مدل‌سازی بر مبنای اکتور وجود دارد اما همگی درستی‌یابی محدودی برای خواص زمانی ارائه می‌دهند. ربکای زمان‌دار یک گسترش از زبان مدل‌سازی سطح بالای ربکا و به طور خالص مبتنی بر اکتور است که در آن، امکان توصیف رفتار اکتورها با قیود زمانی فراهم شده است.هر چند که ربکا دارای یک مجموعه ابزار قوی برای تحلیل سیستم است، اما برای ربکای زمان‌دار امکانات محدود تحلیل وجود دارد. در این پژوهش با ارائه‌ی یک معنای صوری قابل اجرا از ربکای زمان‌دار در ماد بی‌درنگ، امکان استفاده از ابزار ماد بی‌درنگ برای تحلیل سیستم‌های مدل شده با ربکای زمان‌دار فراهم شده است. زبان ماد بی‌درنگ گسترش‌یافته‌ی زمانیِ زبانِ بر مبنای منطق بازنویسیِ ماد است و طیف گسترده‌ای از روش‌های تحلیل از جمله شبیه‌سازی، دسترس‌پذیری، وارسی‌مدل زمان‌محدود منطق‌زمانی‌خطی بدون زمان و وارسی‌مدل‌زمانی منطق‌محاسباتی‌درختی‌زمانی را پشتیبانی می‌کند. منطق بازنویسی یک منطق قدرتمند و پلی برای ایجاد هم‌ارزی بین محاسبه و منطق است. ارائه‌ی این معنای صوری قابل اجرا برای ربکای زمان‌دار در ماد بی‌درنگ، منتج به توصیف مدل محاسباتی اکتور زمان‌دار در منطق بازنویسی شده و همچنین به عنوان یک معناشناسی عملیاتی ساختاری جدید برای ربکای زمان‌دار می‌تواند محسوب شود. همچنین در این پژوهش، کاربرد نگاشت معنایی ارائه شده برای یک مطالعه موردی در حوزه‌ی پروتکل‌های شبکه‌های بی‌سیم ارزیابی شده است. واژه‌های کلیدی: وارسی‌مدل، مدل اکتور، ربکای زمان‌دار، منطق بازنویسی، ماد بی‌درنگ، سیستم‌های همروند، سیستم‌های بی‌درنگ.
- Abstract
- The actor model is one of the useful models for asynchronous and distributed computation, and has been extended to real-time systems. There are some modeling and programming languages based on this model, however, none of them fully support verifying timed properties. Timed Rebeca is a timed extension of the high-level actor-based modeling language Rebeca. Although Rebeca is supported by a rich verification toolset, Timed Rebeca has not had a timed model checker. In this research, we provide a formal semantics of Timed Rebeca in Real-Time Maude. Real-Time Maude extends the rewriting-logic-based Maude language and supports formal analysis of real-time systems. Furthermore, we present the Maude rewriting rules for Timed Rebeca which can be considered as the operational semantics of that. We have automated this translation from Timed Rebeca to Real-Time Maude, allowing our Timed Rebeca models to be automatically analyzed using Real-Time Maude's simulation and reachability analysis. We also can use untimed LTL and timed CTL model checker tool of Real-Time Maude. The presented language translation enables a formal model-based methodology which combines the convenience of intuitive modeling in Timed Rebeca with formal verification in Real-Time Maude and uses the advantageous of power of rewrite logic. At the end, we illustrate this methodology with a case study in the area of wireless network protocols. Keywords: Model Checking, Actor Model, Timed Rebeca, Rewrite Logic, Real-Time Maude, Concurrent Systems, Real-Time Systems.
