برای لینوکس، مکانیزمی برای تأیید صحت هسته پیشنهاد شده است

برای گنجاندن در هسته لینوکس 5.20 (شاید شعبه شماره 6.0 باشد)، مجموعه ای از وصله ها با پیاده سازی مکانیسم RV (Runtime Verification) پیشنهاد شده است که ابزارهایی برای بررسی عملکرد صحیح در سیستم های بسیار قابل اعتماد ارائه می دهد که تضمین کننده عدم وجود شکست راستی‌آزمایی در زمان اجرا با اتصال کنترل‌کننده‌ها به نقاط ردیابی انجام می‌شود که پیشرفت واقعی اجرا را در برابر یک مدل قطعی مرجع از پیش تعیین‌شده خودکار که رفتار مورد انتظار سیستم را تعریف می‌کند، بررسی می‌کند.

اطلاعات حاصل از نقاط ردیابی مدل را از یک حالت به حالت دیگر منتقل می کند و اگر حالت جدید با پارامترهای مدل مطابقت نداشته باشد، یک هشدار ایجاد می شود یا هسته در حالت "هراس" قرار می گیرد (انتظار می رود سیستم های با قابلیت اطمینان بالا تشخیص دهند. و به چنین شرایطی پاسخ دهند). مدل خودکار، که انتقال از یک حالت به حالت دیگر را تعریف می کند، به فرمت "نقطه" (graphviz) صادر می شود، پس از آن با استفاده از ابزار dot2c به یک نمایش C ترجمه می شود، که به شکل یک ماژول هسته بارگذاری می شود. انحرافات پیشرفت اجرا را از مدل از پیش تعریف شده ردیابی می کند.

برای لینوکس، مکانیزمی برای تأیید صحت هسته پیشنهاد شده است

بررسی مدل در زمان اجرا به عنوان روشی سبک‌تر و آسان‌تر برای تأیید اجرای صحیح در سیستم‌های حیاتی، تکمیل کننده روش‌های تأیید قابلیت اطمینان کلاسیک مانند بررسی مدل و اثبات‌های ریاضی انطباق کد با مشخصات ارائه‌شده در فرمال، قرار می‌گیرد. زبان از جمله مزایای RV، توانایی ارائه تأیید دقیق بدون اجرای جداگانه کل سیستم در یک زبان مدلسازی، و همچنین پاسخ انعطاف پذیر به رویدادهای پیش بینی نشده، به عنوان مثال، برای جلوگیری از انتشار بیشتر یک شکست در سیستم های بحرانی است.

منبع: opennet.ru

اضافه کردن نظر