عنوان پایان‌نامه
بررسی روشهای تجرید مدلهای ربکا به منظور درستی یابی صوری
- رشته تحصیلی
- مهندسی کامپیوتر -نرم افزار
- مقطع تحصیلی
- کارشناسی ارشد
- محل دفاع
- کتابخانه مرکزی -تالار اطلاع رسانی شماره ثبت: 38782;کتابخانه دانشکده برق و کامپیوتر شماره ثبت: E1493
- تاریخ دفاع
- ۱۲ شهریور ۱۳۸۷
- دانشجو
- حمیده صبوری قمی
- چکیده
- چکیده استفاده از درستی یابی صوری رهیافتی مطمئن برای ایجاد سیستم های قابل اطمینان است. از طرفی درستی یابی سیستم های بزرگ به دلیل انفجار فضای حالت با مشکل مواجه است. بنابراین برای بهره مندی از مزایای درستی یابی در این سیستم ها لازم است که ابتدا این مشکل رفع شود. استفاده از روش های تجرید مدل در درستی یابی یکی از راه های مقابله با مشکل انفجار فضای حالت است. تجرید داده، تجرید براساس تفسیر مجرد، تجرید گزاره، درستی یابی پیمانه ای و برش دادن نمونه هایی از روش های تجرید مدل می باشند. در میان این روش ها، برش دادن برنامه به دلیل خودکار بودن، حفظ ویژگی های مدل به صورت قوی و قابل ترکیب بودن با دیگر روش های تجرید، روش مناسبی برای تجرید مدل خواهد بود. برای برش دادن یک مدل باید ابتدا آن مدل از نظر جریان کنترل و جریان داده تحلیل شود. حاصل تحلیل جریان کنترل مدل ها گراف جریان کنترل است که از آن برای تحلیل داده نیز استفاده می شود. در قدم بعدی یک گراف وابستگی برای مدل تولید می شود که نشان دهنده وابستگی های موجود میان جملات مدل است. در مرحله نهایی با اعمال یک الگوریتم دسترس پذیری روی این گراف یک برش از مدل بدست می آید. در این پایان نامه در ابتدا تکنیک برش دادن ایستا برای مدل های ربکا ارائه شده است. ربکا یک زبان مبتنی بر اکتور است که برای مدلسازی سیستم های همروند استفاده می شود. برای تحلیل جریان کنترل مدل های ربکا، گراف های جریان کنترل ربکا و جریان کنترل تخمینی ربکا معرفی شده اند. برای مدلسازی وابستگی های موجود میان جملات مدل ها، گراف وابستگی ربکا و گراف وابستگی مبتنی بر ربک ارائه شده اند. این گراف ها (جریان کنترل و وابستگی) منطبق بر مفاهیم معنایی زبان ربکا می باشند. از آنجایی که برش دادن ایستا معمولا برش های بزرگی از مدل ایجاد می کند، دو تکنیک جدید برش دادن قدم به قدم و برش دادن کراندار، در این پایان نامه پیشنهاد شده اند. برش دادن قدم به قدم در ابتدا حد بالایی از مدل را به عنوان برش محاسبه می کند و در مراحل بعد براساس نتیجه درستی یابی (برقراری یا نقض ویژگی و مثال نقض تولید شده) برش را پالایش می کند. برش دادن کراندار با استفاده از جملات تخصیص غیرقطعی در ربکا، حدودی را برای الگوریتم برش مشخص می کند. همچنین در این پایان نامه یک تکنیک ساده برای برش دادن مدل¬ها برای تشخیص بن بست نیز پیشنهاد شده است (تکنیک های دیگر برش دادن، یک برش از مدل را برای بررسی یک ویژگی خاص محاسبه می کنند). در انتها نیز کاربردی بودن تکنیک های معرفی شده با اعمال آنها روی تعدادی مثال و ارائه نتایج بدست آمده، نشان داده شده است.
- Abstract
- Abstract Formal verification is a promising approach for developing more reliable software. On the other hand, verification of large systems may lead to state space explosion. Therefore, for taking advantage of verification, this problem should be solved first. Using model abstraction techniques is a possible solution for this problem. These techniques include data abstraction, abstract interpretation based abstraction, predicate abstraction, modular verification and program slicing. Among these techniques program slicing is more appropriate due to its automatic processing, strong property preservation and capability of combination with other abstraction techniques. The first step in slicing is analyzing the control flow and data flow of a model. Control flow analysis leads to a control flow graph which will be used for data flow analysis later. In the next step, a dependency graph should be constructed showing the dependencies among the statements. Finally the slice can be computed by applying a reachability algorithm on the dependency graph. In this work, first a static slicing technique is introduced for Rebeca models. Rebeca is an actor-based language which is used for modeling concurrent systems. For analyzing the control flow of Rebeca models two special graphs are introduced: Rebeca control flow graph and Approximated Rebeca control flow graph. For modeling the dependencies among the statements, Rebeca dependence graph and Rebec-based dependence graph are presented. These graphs (control flow and dependency graphs) are based on Rebeca semantics. As the static slicing usually produces large slices, two other slicing-based reduction techniques, step-wise slicing and bounded slicing, are proposed as simple novel ideas. Step-wise slicing first generates slices overapproximating the behavior of the original model and then refines it, and bounded slicing is based on the semantics of non-deterministic assignments in Rebeca. We also propose a static slicing algorithm for deadlock detection (in absence of any particular property). The applicability of these techniques is checked by applying them to several case studies which are included in this paper. Similar techniques can be applied on the other actor-based languages.
