Linux yadrosiga 5.20 (ehtimol, filial 6.0 raqami bilan raqamlangan bo'lishi mumkin) kiritish uchun RV (Runtime Verification) mexanizmini amalga oshirish bilan bir qator yamoqlar taklif etiladi, bu yuqori ishonchli tizimlarda to'g'ri ishlashini tekshirish uchun vositalarni taqdim etadi. muvaffaqiyatsizliklarning yo'qligi. Tasdiqlash ish vaqtida bajarilishning amaldagi borishini tizimning kutilayotgan harakatini aniqlaydigan avtomatning oldindan belgilangan mos yozuvlar deterministik modeliga nisbatan tekshiradigan kuzatuv nuqtalariga ishlovchilarni biriktirish orqali amalga oshiriladi.
Kuzatuv nuqtalaridan olingan ma'lumotlar modelni bir holatdan ikkinchi holatga o'tkazadi va agar yangi holat model parametrlariga mos kelmasa, ogohlantirish hosil bo'ladi yoki yadro "vahima" holatiga joylashtiriladi (yuqori ishonchlilik tizimlari aniqlanishi kutilmoqda). va bunday vaziyatlarga javob bering). Bir holatdan ikkinchi holatga o'tishni belgilaydigan avtomat modeli "nuqta" formatiga (graphviz) eksport qilinadi, shundan so'ng u dot2c yordam dasturi yordamida C ko'rinishiga tarjima qilinadi, u yadro moduli ko'rinishida yuklanadi. oldindan belgilangan modeldan bajarish jarayonining og'ishlarini kuzatib boradi.
Ishlash vaqtidagi modelni tekshirish muhim tizimlarda to'g'ri bajarilishini tekshirishning engilroq va oson bajariladigan usuli sifatida joylashtirilgan bo'lib, modelni tekshirish va rasmiy hujjatda berilgan spetsifikatsiyalarga kod muvofiqligini matematik isbotlash kabi klassik ishonchlilikni tekshirish usullarini to'ldiradi. til. RV ning afzalliklari orasida butun tizimni modellashtirish tilida alohida amalga oshirmasdan qat'iy tekshirishni ta'minlash, shuningdek, kutilmagan hodisalarga moslashuvchan javob berish, masalan, muhim tizimlarda nosozlikning keyingi tarqalishini blokirovka qilish imkoniyati mavjud.
Manba: opennet.ru