Для ўключэння ў склад ядра Linux 5.20 (магчыма, галінка атрымае нумар 6.0) прапанаваны набор патчаў з рэалізацыяй механізму RV (Runtime Verification), які прадстаўляе сродкі для праверкі карэктнасці працы на высоканадзейных сістэмах, якія гарантуюць адсутнасць збояў. Праверка вырабляецца падчас выканання праз прымацаванне апрацоўшчыкаў да кропак трасіроўкі, якія звяраюць фактычны ход выканання з загадзя вызначанай эталоннай дэтэрмінаваных мадэллю аўтамата, які вызначае чаканыя паводзіны сістэмы.
Інфармацыя ад кропак трасіроўкі перакладае мадэль з аднаго стану ў іншы, і калі новы стан не адпавядае параметрам мадэлі, генеруецца папярэджанне ці ядро перакладаецца ў стан panic (маецца на ўвазе, што высоканадзейныя сістэмы будуць вызначаць падобныя сітуацыі і рэагаваць на іх). Мадэль аўтамата, якая вызначае пераходы з аднаго стану ў іншы, экспартуецца ў фармат «dot» (graphviz), пасля чаго транслюецца пры дапамозе ўтыліты dot2c ва ўяўленне на мове Сі, якое загружаецца ў форме модуля ядра, які адсочвае адхіленні ходу выканання ад вызначанай мадэлі.
Зверка з мадэллю падчас выканання пазіцыянуецца як больш легкаважны і просты для рэалізацыі на практыцы спосаб пацверджання карэктнасці выканання на крытычна важных сістэмах, які дапаўняе класічныя метады пацверджання надзейнасці, такія як праверка мадэлі і матэматычныя доказы адпаведнасці кода спецыфікацыям, зададзеным на фармальнай мове. З добрых якасцяў RV называецца магчымасць забяспечыць строгую верыфікацыю без асобнай рэалізацыі ўсёй сістэмы на мове мадэлявання, а таксама гнуткае рэагаванне на непрадбачаныя падзеі, напрыклад, для блакавання далейшага распаўсюджвання збою ў крытычна важных сістэмах.
Крыніца: opennet.ru