کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
423364 | 685212 | 2008 | 19 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
The Verification of rCOS Using Spin 1
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله

چکیده انگلیسی
The rCOS is a relational object-based language with a precise observation-oriented semantics. It can capture key features of object model including subtypes, visibility, inheritance, polymorphism and so on. To analyze the model specified by rCOS, we propose a verification approach to check whether those properties such as the assertion, invariant of class and method contracts hold. The Spin model checker is used in this approach. To enhance the ability of description of concurrency, we extend the original rCOS with parallel structure and synchronization mechanism. The Promela model is constructed from rCOS specification with non-trivial mapping rules. We also present a case study to show how our approach works.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Electronic Notes in Theoretical Computer Science - Volume 207, 10 April 2008, Pages 49-67
Journal: Electronic Notes in Theoretical Computer Science - Volume 207, 10 April 2008, Pages 49-67