نگاشت صوری مدل های ربکای زماندار به لینگوافرانکا با حفظ قطعیّت رفتاری [پايان نامه فارسي]
علی سرمدی
| شناسگر رکورد: | ۵۲۵۱۳ |
| رشته تحصیلی: | علوم داده |
| عنوان: | نگاشت صوری مدل های ربکای زماندار به لینگوافرانکا با حفظ قطعیّت رفتاری |
| نويسنده: | علی سرمدی |
| استاد راهنما : | دکتر حسین حجت |
| مقطع تحصیلی : | کارشناسی ارشد |
| دانشگاه : | خاتم |
| تاریخ دفاع : | ۱۴۰۴ |
| چکیده: | سامانه های سایبرـفیزیکی و تعبیه شده برای کاربردهای حساس مانند کنترل صنعتی، رباتیك و پزشکی به رفتارهای قابل پیش بینی و تحلیل پذیر نیاز دارند. زبان ربکا و گونه ی زمان دار آن ابزار ارزشمندی برای مدلسازی و بررسی صوری این سامانه ها فراهم میکنند، اما مستقیما˝ قابلیت اجرا بر بسترهای واقعی را ندارند. در مقابل، چارچوب لینگوافرانکا با محوریت زمان منطقی و اجرای قطعی طراحی شده است، ولی زنجیره ی ابزار و روش های تحلیل رسمی آن هنوز در حال تکامل است. این پژوهش با هدف پل زدن میان تحلیل صوری در ربکای زماندار و اجرای قطعی در لینگوافرانکا انجام شده است. در این کار دو زیرمجموعه ی رسمی تعریف شدند TR-Lite-P :از ربکای زمان دار با اولویت های محلی برای تضمین قطعیتّ در سطح اکتور، و LF-Cpp-Q از لینگوافرانکا با صف محرك داخلی و ساختار تخت برای واکنشگرها. برای هر دو زیرزبان قواعد معناشناسی عملیاتی یکنواخت ارائه گردید تا رفتارهای پیام رسانی و گذر زمان به صورت شفاف مقایسه شوند. سپس برهان هم ارزی دوطرفه نشان داد که گام های اصلی شامل ارسال، انتساب، شرطی، برداشت پیام/محرك و پیشروی زمان در دو سوی نگاشت به طور گام به گام متناظر هستند. بر اساس این چارچوب نظری، یك ابزار مترجم در جاوا توسعه یافت که نگاشته ای اصلی از مدل های ربکا به کدهای لینگوافرانکا را عملی میکند. این ابزار تبدیل را پیاده سازی میکند و کدهای خروجی را برای زمان اجرای C++ لینگوافرانکا آماده می سازد. نتایج تجربی روی الگوهای شاخص نشان می دهد که مدل های ربکا یا ذاتا˝ از طریق وابستگی علّی قطعی اند یا با استفاده از نشانه گذاری @priority قطعی میشوند و برنامه های لینگوافرانکا حاصل همان ردپاهای مشاهده پذیر را دنبال می کنند. این پژوهش نشان می دهد که میتوان مدل های ربکای زمان دار را بدون بازاعتبارسنجی به برنامه های لینگوافرانکا ترجمه کرد، مشروط بر اینکه مدل ها در محدوده ی قطعی تعریف شده باقی بمانند. بدین ترتیب، یك مسیر از مدلسازی صوری تا اجرای قطعی فراهم می شود که میتواند در توسعه ی سامانه های حساس و ایمنی حیاتی به کار گرفته شود. |
| واژگان کلیدی: | ربکا زماندار،لینگوافرانکا،قطعیتّ،ترجمه ی حافظ معنا،هم ارزی دوطرفه |
| شماره ثبت | جزء | نسخه | جلد | بخش | قسمت | مرجع | شماره بازیابی | در دست امانت | تاریخ بازگشت | ملاحظات | |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 284973 | 1 |
جهت مشاهده فایل دیجیتال با حساب کاربریتان وارد شوید
جهت ثبت نظر با حساب کاربری تان وارد شوید