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