کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
10329447 685407 2005 16 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Towards a Small Model Theorem for Data Independent Systems in Alloy
کلمات کلیدی
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
Towards a Small Model Theorem for Data Independent Systems in Alloy
چکیده انگلیسی
Alloy is an extension of first-order logic for modelling software systems. Alloy has a fully automatic analyser which attempts to refute Alloy formulae by searching for counterexamples within a finite scope. However, failure to find a counterexample does not prove the formula correct. A system is data-independent in a type T if the only operations allowed on variables of type T are input, output, assignment and equality testing. This paper gives a theorem in a language closely related to Alloy, which applies to models of data-independent systems. The theorem calculates for such types T a threshold size. If no counterexamples are found at the threshold, the theorem guarantees that increasing the scope on T beyond the threshold still yields no counterexamples, and can complete the analysis for data-independent systems.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Electronic Notes in Theoretical Computer Science - Volume 128, Issue 6, 23 May 2005, Pages 37-52
نویسندگان
,