عنوان پایان‌نامه
مدل سازی و درستی یابی سیستم های اکتور با توپولوژی پویا
- رشته تحصیلی
- مهندسی کامپیوتر -نرم افزار
- مقطع تحصیلی
- کارشناسی ارشد
- محل دفاع
- کتابخانه مرکزی پردیس 2 فنی شماره ثبت: E 2462;کتابخانه مرکزی -تالار اطلاع رسانی شماره ثبت: 63589
- تاریخ دفاع
- ۲۲ دی ۱۳۹۲
- دانشجو
- پوریا ملتی
- استاد راهنما
- رامتین خسروی
- چکیده
- در مدل محاسباتی اکتور، تمامی محاسبات انجام شده توسط هر اکتور در قالب سه امکان اولیه‌ی ایجاد اکتورها، ارسال پیام‌ها به دیگر اکتورها و تغییر حالت داخلی اکتور، بیان می‌شوند. متأسفانه، در حوزه‌ی وارسی مدل، چه در بخش مدل‌سازی و چه در بخش توصیف خصایص، پشتیبانی مناسبی برای سیستم‌های پویای مبتنی مدل اکتور، یعنی آن دسته از سیستم‌ها که در آن‌ها از امکان ایجاد اکتورها و تغییر شبکه‌ی ارتباطی میان آن‌ها به صورت پویا (در حین اجرای سیستم یا مدل) استفاده می‌شود وجود ندارد. در این پژوهش، به ارائه‌ی پشتیبانی مناسب از این سیستم‌ها پرداخته‌ایم. بدین منظور، در زمینه‌ی مدل‌سازی، نحو و معناشناسی یک زبان موجود برای مدل‌سازی سیستم‌های مبتنی بر مدل اکتور (زبان ربکا) را گسترش داده‌ایم. زبان حاصل از نحو و معناشناسی گسترش یافته، امکان ایجاد اکتورها و تغییر شبکه‌ی ارتباطی میان اکتورها، به صورتی طبیعی، را ارائه می‌دهد. همچنین، در زمینه‌ی پشتیبانی از توصیف خصایص ناظر بر مدل‌های پویا، یک منطق زمانی جدید به نام لیتل را معرفی و پیشنهاد کرده‌ایم. این منطق زمانی، امکان استفاده از سورها بر روی اشیاء موجود در حالات مدل را ارائه می‌دهد. به علاوه، با استفاده از این منطق، درتوصیف خصایص، می‌توان شبکه‌ی ارجاعات میان اکتورها را، به منظور دسترسی به مقادیر متغیرهای مورد نظر، پیمایش نمود. کارآمدی زبان مدل‌سازی و منطق توصیف خصایص ارائه شده برای وارسی مدل سیستم‌های پویا، در قالب دو نمونه مطالعه نشان داده شده است.
- Abstract
- In the actor model, the logic of computation for each actor is defined, solely, in terms of three basic capabilities: creation of new actors, sending messages to other actors and changing the actor's local state. Unfortunately, currently, in the field of model checking, both in the modeling and property specification areas, support for dynamic actor-based systems, i.e. those in which, during the execution of the system (dynamically), new actors are created or the web of relationships between actors is manipulated, is less than satisfactory. This thesis is dedicated to providing proper support for the model checking of such systems. To this end, in the modeling area, we have overhauled the syntax and semantics of rebeca, an existing language designed for the formal modeling of actor-based systems. Using our overhauled language, dynamic creation of actors and the evolution of the graph of relationships between them, is possible, in a natural way. In the property specification area, we propose LeeTL, a new temporal logic that supports quantifications over model objects. Using LeeTL, it is also possible to traverse the web of references between actors to gain access to specific variables during property specification. The suitability of the overhauled modeling language and the proposed property specification logic, for model checking dynamic actor-based systems, is demonstrated using two case-studies.
