دانلود رایگان ترجمه مقاله کاهش های مبتنی بر برش برای Rebeca (نشریه الزویر 2010) (ترجمه رایگان – برنزی ⭐️)

کاهش های مبتنی بر برش برای Rebeca

Slicing-based Reductions for Rebeca

چکیده
1. مقدمه
2 کار مرتبط
3 مقدمات
3-1 Rebecca

چکیده
برش, یک تکنیک تجزیه و تحلیل برنامه است که می توان برای کاهش اندازه مدل و جلوگیری از انفجار حالت در چک کردن مدل استفاده نمود. در این کار, یک روش برش استاتیک برای کاهش مدل های Rebecca با توجه به یک ویژگی ارائه شده است. برای استفاده از تکنیک های برش، نمودار وابستگی Rebecca (RDG) معرفی شده است. به این دلیل که برش استاتیک معمولاً قطعه های بزرگ را تولید می کند، دو تکنیک دیگر کاهش مبتنی بر برش، برش گام به گام و برش محدود، به عنوان ایده های ساده جدید پیشنهاد شده اند. برش گام به گام تولید, قطعاتی را برای تخمین بیش از حد رفتار مدل اصلی تولید می کند و سپس آن را تصحیح می کند و برش محدود بر اساس معناشناسی تکالیف غیر-قطعی در Rebecca است. ما همچنین یک الگوریتم برش استاتیک را برای تشخیص بن بست پیشنهاد می دهیم (در غیاب هر ویژگی خاصی). قابلیت کاربرد این تکنیک ها با کاربرد آنها برای چند مطالعه موردی که در این مقاله گنجانده شده است بررسی می شود. تکنیک های مشابه را می توان در دیگر زبان های مبتنی بر-عامل اعمال نمود.
1- مقدمه
چک کردن مدل [4] یک روش تأیید رسمی برای تایید سیستم های همزمان در برابر تعدادی از مشخصات است و می تواند برای توسعه سیستم های قابل اطمینان تر استفاده شود. مشکل اصلی چک کردن مدل, مشکل انفجار فضای حالت است و بسیاری از تکنیک ها برای غلبه بر این مشکل توسعه یافته اند. این روشها عبارتند از: تفسیر انتزاعی [5]، انتزاع داده [9]، انتزاع گزاره [12]، برش [31]، مرتبه جزئی [23] و کاهش های تقارن [15].
برای استفاده از روش چک کردن مدل، نخست باید از یک زبان مدل سازی برای نشان دادن رفتار سیستم استفاده نمود. Rebecca [27] (زبان واکنشی اشیاء) یک زبان مبتنی بر-عامل با یک پایه رسمی برای مدل سازی و بررسی سیستم های همزمان و توزیع شده است که در تلاش برای پر کردن شکاف بین روش های تأیید رسمی و برنامه های کاربردی واقعی طراحی شده است. در [26], اجزا برای زبان Rebecca به منظور بسته بندی محکم اشیاء واکنشی جفت شده معرفی شده اند. این زبان با مجموعه ای از ابزار های چک کردن مدل [17،28،29] پشتیبانی می شود.
برش استاتیک [31], دستوراتی را از یک برنامه گرفته است که دارای اثر مستقیم یا غیر مستقیم بر محاسبات خاص است. یکی از رویکردهای اصلی برای برش, استفاده از تجزیه و تحلیل قابلیت دسترسی در نمودار وابستگی برنامه است.
برای مدل های برش Rebecca, یک گراف وابستگی باید ابتدائاً ساخته شود. برای این منظور, ما گراف وابستگی خاص را بر اساس معناشناسی Rebecca معرفی می کنیم. این نمودار دارای پیچیدگی کمتر از نمودارهای وابستگی موجود است که دلیل آن, ماهیت ناهمزمان ارتباطات، اجرای اتمی سرورهای پیام، عدم وجود متغیرهای به اشتراک گذاشته و عدم تماس های رویه است (از این رو هیچ نیازی به لبه های تداخل و یا خلاصه مورد بحث در [19] وجود ندارد) . علاوه بر این، هر چند Rebecca, یک زبان مبتنی بر-شی است، نباید با پیچیدگی های نمودارهای وابستگی طراحی شده برای زبان های شی گرا سرو کار داشته باشیم، زیرا ویژگی هایی مانند وراثت و چند ریختی در زبان گنجانده نشده اند. در مورد مدل های مبتنی بر جزء, زیرگراف مربوطه از هر یک از مؤلفه ها را می توان ذخیره نمود و زمانی که یک جزء در مدل دیگری به نظر می رسد, مورد استفاده مجدد قرار داد.
برای محاسبه برش از نمودار حاصل، چهار الگوریتم مختلف در این مقاله ارائه شده است. اولین الگوریتم, الگوریتم قابلیت دسترسی سنتی است که برای برش استاتیک استفاده می شود. الگوریتم دوم بر اساس یک ایده ساده بر اساس جدید است و زمانی استفاده می شود که ما می خواهیم یک مدل را در برابر بن بست چک کنیم (بر خلاف الگوریتم های برش منظم، هیچ نیازی به مشخص نمودن یک ویژگی در اینجا وجود ندارد). ایده کار, حذف دستوراتی است که هیچ تاثیری در هیچ بیانیه ای دیگری ندارند.
در الگوریتم برش سوم، برش گام به گام، یک تخمین بیش از حد از مدل اصلی محاسبه می شود و سپس بر اساس نتیجه تایید، مدل کاهش یافته در صورت نیاز اصلاح می شود. این الگوریتم توسط گنجاندن متغیرهای ویژگی در مدل شروع می شود. متغیرهایی که دارای اثر مستقیم بر ارزش متغیرهای ویژگی هستند نیز در مدل گنجانده می شوند. این متغیرها یک مقدار را با استفاده از یک انتساب غیر قطعی در مدل کاهش یافته می گیرند. متغیرهای دیگر از مدل حذف می شوند. سپس, مدل کاهش یافته تایید می شود و در صورتی که یک مثال نقض جعلی پیدا شود، مدل با گنجاندن متغیرهای بیشتری در آن اصلاح می شود.

Abstract

Abstract Slicing is a program analysis technique which can be used for reducing the size of the model and avoid state explosion in model checking. In this work a static slicing technique is proposed for reducing Rebeca models with respect to a property. For applying the slicing techniques, the Rebeca dependence graph (RDG) is introduced. 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.

1- Introduction

Model checking [4] is a formal verification technique for verifying concurrent systems against a number of specifications and can be used for developing more reliable systems. The main problem of model checking is the state space explosion problem and many techniques are developed to overcome this problem. These techniques include: abstract interpretation [5], data abstraction [9], predicate abstraction [12], slicing [31], partial order [23] and symmetry reductions [15].

To take advantage of model checking technique, one must first use a modeling language to represent the behavior of the system. Rebeca [27] (Reactive Objects Language) is an actor-based language with a formal foundation for modeling and verifying concurrent and distributed systems, which is designed in an effort to bridge the gap between formal verification approaches and real applications. In [26] components are introduced for Rebeca language to encapsulate the tightly coupled reactive objects. This language is supported by a set of model checking tools [17,28,29].

Static slicing [31] extracts statements from a program which have a direct or indirect effect on a particular computation. One of the main approaches for slicing is using reachability analysis on program dependence graph.

For slicing Rebeca models a dependency graph should be constructed first. For this purpose we introduced a special dependency graph based on Rebeca semantics. This graph is less complicated than existing dependency graphs, due to the asynchronous nature of communication, atomic execution of message servers, absence of shared variables and absence of procedure calls (hence there is no need for interference or summary edges discussed in [19]). In addition, although Rebeca is an object-based language, we should not deal with complexities of dependence graphs designed for object-oriented languages, as features like inheritance and polymorphism are not included in the language. In the case of component-based models the corresponding subgraph of each component can be saved and reused when a component appears in another model.

For computing the slice from the resulted graph, four different algorithms are presented in this paper. The first one is the traditional reachability algorithm which is used for static slicing. The second algorithm is based on a simple novel idea and is used when we want to check a model against deadlock (unlike regular slicing algorithms there is no need to specify a property here). The idea is eliminating the statements that have no effect on any other statements.

In the third slicing algorithm, step-wise slicing, an overapproximation of the original model is computed and then based on the verification result, the reduced model is refined if needed. This algorithm starts by including the property variables in the model. Variables which have a direct effect on the value of the property variables, are also included in the model. These variables take a value using a nondeterministic assignment, in the reduced model. The other variables are eliminated from the model. Then, the reduced model is verified and if a spurious counterexample is found, the model is refined by including more variables in it..

کاهش های مبتنی بر برش برای Rebeca

Slicing-based Reductions for Rebeca