دانلود رایگان ترجمه مقاله کاهش های مبتنی بر برش برای Rebeca (نشریه الزویر 2010) (ترجمه رایگان – برنزی ⭐️)
این مقاله انگلیسی ISI در نشریه الزویر در 9 صفحه در سال 2010 منتشر شده و ترجمه آن 16 صفحه میباشد. کیفیت ترجمه این مقاله رایگان – برنزی ⭐️ بوده و به صورت ناقص ترجمه شده است.
دانلود رایگان مقاله انگلیسی + خرید ترجمه فارسی | |
عنوان فارسی مقاله: |
کاهش های مبتنی بر برش برای Rebeca |
عنوان انگلیسی مقاله: |
Slicing-based Reductions for Rebeca |
|
مشخصات مقاله انگلیسی (PDF) | |
سال انتشار | 2010 |
تعداد صفحات مقاله انگلیسی | 16 صفحه با فرمت pdf |
رشته های مرتبط با این مقاله | مهندسی کامپیوتر |
گرایش های مرتبط با این مقاله | معماری سیستم های کامپیوتری و مهندسی نرم افزار |
چاپ شده در مجله (ژورنال) | یادداشت های الکترونیکی در علوم نظری کامپیوتری – Electronic Notes in Theoretical Computer Science |
کلمات کلیدی | برش، زبان های مبتنی بر-عامل، Rebecca، چک کردن مدل، تایید، کاهش |
رفرنس | دارد ✓ |
کد محصول | F1411 |
نشریه | الزویر – Elsevier |
مشخصات و وضعیت ترجمه فارسی این مقاله | |
وضعیت ترجمه | انجام شده و آماده دانلود |
تعداد صفحات ترجمه تایپ شده با فرمت ورد با قابلیت ویرایش | 9 صفحه (2 صفحه رفرنس انگلیسی) با فونت 14 B Nazanin |
ترجمه عناوین تصاویر و جداول | ترجمه شده است ✓ |
ترجمه متون داخل تصاویر | ترجمه نشده است ☓ |
ترجمه متون داخل جداول | ترجمه نشده است ☓ |
درج تصاویر در فایل ترجمه | درج شده است ✓ |
درج جداول در فایل ترجمه | درج شده است ✓ |
کیفیت ترجمه | کیفیت ترجمه این مقاله پایین میباشد |
توضیحات | ترجمه این مقاله به صورت ناقص انجام شده است. |
فهرست مطالب |
چکیده |
بخشی از ترجمه |
چکیده |
بخشی از مقاله انگلیسی |
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 |
|