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

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