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

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