کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
4951836 | 1441614 | 2017 | 22 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
On the verification of SCOOP programs
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
کلمات کلیدی
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
![عکس صفحه اول مقاله: On the verification of SCOOP programs On the verification of SCOOP programs](/preview/png/4951836.png)
چکیده انگلیسی
In this paper we focus on the development of a unifying framework for the formal modeling of an object oriented-programming language, its underlying concurrency model and their associated analysis tools. More precisely, we target SCOOP - an elegant concurrency model, recently formalized based on Rewriting Logic (RL) and Maude. SCOOP is implemented in Eiffel and its applicability is demonstrated also from a practical perspective, in the area of robotics programming. Our contribution consists of devising and integrating an alias analyzer and a Coffman deadlock detector under the roof of the same RL-based semantic framework of SCOOP. This enables using the Maude rewriting engine and its LTL model-checker “for free,” in order to perform the analyses of interest. We discuss the limitations of our approach for model-checking deadlocks and provide possible workarounds for the state space explosion problem. On the aliasing side, we propose an extension of a previously introduced alias calculus based on program expressions, to the setting of unbounded program executions. Moreover, we devise a corresponding executable specification easily implementable on top of the SCOOP formalization. An important property of our extension is that, in non-concurrent settings, the corresponding alias expressions can be over-approximated in terms of a notion of regular expressions. This further enables us to derive an algorithm for computing a sound over-approximation of the “may aliasing” information, where soundness stands for the lack of false negatives.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Science of Computer Programming - Volume 133, Part 2, 1 January 2017, Pages 194-215
Journal: Science of Computer Programming - Volume 133, Part 2, 1 January 2017, Pages 194-215
نویسندگان
Georgiana Caltais, Bertrand Meyer,