عنوان پایان‌نامه
مدلسازی و وارسی مدل سیستمهای احتمالی مبتنی بر اکتور
- رشته تحصیلی
- مهندسی کامپیوتر -نرم افزار
- مقطع تحصیلی
- کارشناسی ارشد
- محل دفاع
- کتابخانه پردیس 2 فنی شماره ثبت: E 2157;کتابخانه مرکزی -تالار اطلاع رسانی شماره ثبت: 55813
- تاریخ دفاع
- ۲۷ شهریور ۱۳۹۱
- دانشجو
- مهسا ورشوساز
- استاد راهنما
- رامتین خسروی
- چکیده
- از آنجایی که طیف وسیعی از سیستم‌ها دارای رفتار احتمالی و غیرقطعی هستند، درستی‌یابی کمّی یکی از زمینه‌های پرکاربرد در حیطه‌ی درستی‌یابی سیستم‌ها محسوب می‌شود که به ویژه در سال‌های اخیر مورد توجه پژوهشگران در دانشگاه و صنعت قرار گرفته است. یکی از دامنه‌های وسیع کاربرد این دسته روش‌ها، دامنه‌ی سیستمهای توزیع شده و همروند است. با توجه به استفاده‌ی بسیار وسیع و روز‌افزون از این سیستم‌ها مانند شبکه‌های حسگر و سیستمهای مبتنی بر وب تحلیل بسیاری از ویژگی‌های کمّی و کیفی آنها از اهمیت زیادی برخوردار است. از آنجایی که مدلسازی نقطه شروع بسیاری از روش‌های درستی‌یابی است، این مرحله نیازمند دقت قابل توجهی است. استفاده از یک زبان مدلسازی که از سطح تجرید مناسبی برخوردار بوده و دارای ساختارهایی متناظر با مفاهیم و موجودیت‌های دامنه مورد بررسی باشد، تأثیر بسزایی در زمان صرف شده و کیفیت مرحله‌ی مدلسازی خواهد داشت. در این پژوهش، پی‌ربکا که گسترشی از زبان ربکا برای مدلسازی سیستمهای احتمالی مبتنی بر اکتور است معرفی می‌شود. این زبان با نحوی سطح بالا و شبیه به جاوا، مدلسازی سیستمهای توزیع شده‌ی احتمالی را امکان‌پذیر می‌نماید. در این پژوهش نحو زبان ربکا به گونه‌‌‌‌‌‌‌‌ای گسترش داده می‌شود که امکان مدلسازی رفتارهای احتمالی مختلف و همچنین ارسال پیام نامطمئن در سیستم توصیف شده، فراهم شود. به منظور امکان‌پذیر نمودن وارسی مدل‌های پی‌ربکا با استفاده از روش‌های صوری، معناشناسی صوری برای این مدل‌ها بر پایه یک فرآیند تصمیم‌گیری مارکف بیان می‌شود. همچنین روشی مناسب برای وارسی مدل‌های پی‌ربکا با استفاده از وارسی‌کننده‌ی پریزم ارائه می‌گردد. در نهایت سیستم‌هایی احتمالی به عنوان مطالعات موردی توسط پی‌ربکا مدل شده، با استفاده از روش ارائه شده توسط پریزم، وارسی می‌شوند.
- Abstract
- As a broad range of computer systems exhibit probabilistic and nondeterministic behavior, there has been an increasing interest in employing and developing quantitative verification techniques to analyze and evaluate various properties of such systems. Distributed systems have been among motivating domains gaining much attention for application of quantitative techniques. The widespread and rapid growth of distributed systems such as sensor networks, web-based systems, etc., make it worth to analyze various quantitative and qualitative properties about them. As a starting point of analysis, modeling of such systems could take some effort due to structural and behavioral complexities. Thus, using a computational model compatible with the domain can effectively reduce this effort by expressing the concepts and entities of the domain directly. A modeling language based on the proper computational model, avoids putting extra effort to model the basic computations by providing proper primitives and level of abstraction, making the model more readable and maintainable. To this end, we introduce pRebeca which is an extension to the Rebeca language. It is a high-level object-based modeling language based on the actor model, suitable for describing asynchronous distributed systems with probabilistic behavior. We extended Rebeca syntax with some constructs to model probabilistic choice between alternative behavior and unreliable message passing between actors. we also proposed a method to model check pRebeca models by means of the PRISM model checker. We model and model check some probabilistic systems as case studies using pRebeca and the proposed model checking method
