کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
6875546 1441967 2018 24 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
From hidden to visible: A unified framework for transforming behavioral theories into rewrite theories
ترجمه فارسی عنوان
از پنهان به قابل مشاهده: چارچوب یکپارچه برای تبدیل نظریه های رفتاری به نظریه های بازنویسی
کلمات کلیدی
نظریه رفتاری، نظریه بازنویسی، دگرگونی، اموال خطی زمان،
ترجمه چکیده
رسم جبری و تایید روش های موثر و عملی مدل سازی و تایید سیستم های نرم افزاری با استفاده از هر دو روش مدل سازی و تست های قضیه است. در رویکردهای جبری، سیستم را می توان به صورت پنهان به عنوان یک نظریه رفتاری یا به روش قابل ملاحظه ای به عنوان نظریه بازنویسی مدل سازی کرد. رویکردهای متعددی برای تبدیل نظریه های رفتاری به نظریه های بازنویسی برای تطبیق چک کردن مدل و قضیه ثابت شده در تأیید ارائه شده است. در این مقاله، چارچوبی برای تبدیل نظریه های رفتاری به نظریه های بازنویسی پیشنهاد شده است که چهار رویکرد تحول پذیر مرتبط را متحد می کند. در این چارچوب، هر روش رویکرد موجود، می تواند به عنوان یک فرآیند تبدیل نظریه های رفتاری ابتدا به یک کلاس ویژه از نظریه های رفتاری و در نهایت به نظریه های بازنویسی شود. از این منظر، این رویکردهای تحول، تنها در تحول از نظریه های رفتاری عادی به دسته بندی ها متفاوت است، و تبدیل آنها از طبقه بندی به نظریه های بازنویسی اساسا یکسان است. ما ثابت می کنیم که چارچوب تحول، خواص خطی زمان را حفظ می کند. حفاظت از خواص خطی زمان، تضمین می کند که یک مثال مخفی که توسط مدل پیدا می شود و یک ویژگی زمانبندی خطی با یک نظریه بازنویسی تولید شده است، نمونه ای از نمونه در نظریه رفتاری اصلی است که مورد نیاز توسط تایید یکپارچه است.
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش مقاله
از پنهان به قابل مشاهده: چارچوب یکپارچه برای تبدیل نظریه های رفتاری به نظریه های بازنویسی
چکیده انگلیسی
Algebraic formalization and verification are effective and practical ways of modeling and verifying software systems by both model checking and theorem proving techniques. In algebraic approaches, a system can be modeled either in a hidden way as a behavioral theory or in a visible way as a rewrite theory. Several approaches have been proposed to transform behavioral theories into rewrite theories for integrating model checking and theorem proving in verification. In this paper, we propose a framework for transforming behavioral theories into rewrite theories, which unifies four existing related transformation approaches. In this framework, each existing transformation approach can be viewed as a process of transforming behavioral theories first into a special class of behavioral theories and finally into rewrite theories. From this perspective, these transformation approaches differ from each other only in the transformation from ordinary behavioral theories into the classified ones, and their transformations from the classified ones into rewrite theories are essentially the same. We prove that the transformation framework preserves linear-time properties. The preservation of linear-time properties guarantees that a counterexample found by model checking a linear-time property with a generated rewrite theory is also a counterexample in the original behavioral theory, as required by integrated verification.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Theoretical Computer Science - Volume 722, 25 April 2018, Pages 52-75
نویسندگان
, ,