Барои дохил кардан ба ядрои Linux 5.20 (шояд филиал рақамгузорӣ карда шавад 6.0), маҷмӯи часбҳо бо татбиқи механизми RV (Runtime Verification) пешниҳод карда мешавад, ки асбобҳоро барои тафтиши кори дуруст дар системаҳои хеле боэътимод таъмин мекунад, ки набудани нобарориҳо. Санҷиш дар вақти корӣ тавассути замима кардани коркардкунандагон ба нуқтаҳои пайгирӣ, ки пешрафти воқеии иҷроро дар муқоиса бо модели пешакӣ муайяншудаи детерминистии автоматӣ, ки рафтори интизории системаро муайян мекунад, анҷом дода мешавад.
Маълумот аз нуқтаҳои пайгирӣ моделро аз як ҳолат ба ҳолати дигар интиқол медиҳад ва агар ҳолати нав ба параметрҳои модел мувофиқат накунад, огоҳӣ тавлид мешавад ё ядро дар ҳолати "ваҳшат" ҷойгир карда мешавад (системаҳои эътимоднокии баланд интизоранд ва ба чунин ҳолатҳо вокуниш нишон диҳед). Модели автоматӣ, ки гузаришро аз як ҳолат ба ҳолати дигар муайян мекунад, ба формати "нуқта" (graphviz) содир карда мешавад, пас аз он бо истифода аз утилитаи dot2c ба муаррифии C тарҷума карда мешавад, ки он дар шакли модули ядро бор карда мешавад. инҳирофҳои пешрафти иҷроро аз модели пешакӣ муайяншуда пайгирӣ мекунад.
Санҷиши модели вақти корӣ ҳамчун як усули сабуктар ва осонтар иҷрошавандаи тафтиши иҷрои дуруст дар системаҳои муҳими миссия ҷойгир карда шудааст, ки усулҳои классикии санҷиши эътимоднокӣ, ба монанди санҷиши модел ва далелҳои математикии мувофиқати кодро бо мушаххасоти расмӣ пешниҳод мекунад. забон. Дар байни бартариҳои RV қобилияти таъмини санҷиши қатъӣ бидуни татбиқи алоҳидаи тамоми система бо забони моделсозӣ, инчунин вокуниши чандир ба рӯйдодҳои ғайричашмдошт, масалан, пешгирии паҳншавии минбаъдаи нокомӣ дар системаҳои муҳим мебошад.
Манбаъ: opennet.ru