کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
422185 | 685038 | 2008 | 21 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Using Model Checking to Automatically Find Retrieve Relations
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله

چکیده انگلیسی
Downward and upward simulations form a sound and jointly complete methodology for verifying relational data refinement in state-based specification languages such as Z and B. In previous work, we showed how both downward and upward simulation conditions can be discharged using a CTL model checker. The approach was implemented in the SAL tool suite. Given the retrieve relation, each of the simulation conditions can be proven fully automatically. It has been recognised, however, that finding retrieve relations is often very hard. In this paper, we show how it is feasible to use the SAL model checkers to also generate retrieve relations.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Electronic Notes in Theoretical Computer Science - Volume 201, 7 March 2008, Pages 155-175
Journal: Electronic Notes in Theoretical Computer Science - Volume 201, 7 March 2008, Pages 155-175