کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
422468 685094 2008 25 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Completeness of ASM Refinement
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
Completeness of ASM Refinement
چکیده انگلیسی

ASM refinements are verified using generalized forward simulations which allow to refine m abstract operations to n concrete operations with arbitrary m and n. One main difference to data refinement is that ASM refinement considers infinite runs and termination. Since backward simulation does not preserve termination in general, the standard technique of adding history information to the concrete level is not applicable. The powerset construction also adds infinite runs and is therefore not applicable too. This paper shows that a completeness proof is nevertheless possible by adding infinite prophecy information, effectively moving nondetermism to the initial state. Adding such prophecy information can be done on the semantic level, but also by a simple syntactic transformation that removes the choose construct of ASMs. The completeness proof is also ported to give a completeness proof for IO automata.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Electronic Notes in Theoretical Computer Science - Volume 214, 28 June 2008, Pages 25-49