Linuxi 5.20 kernelisse lisamiseks (võib-olla saab haru numbriks 6.0) pakutakse välja paikade komplekt koos RV (Runtime Verification) mehhanismiga, mis pakub tööriistu väga töökindlate süsteemide õige töö kontrollimiseks, mis tagavad ebaõnnestumiste puudumine. Kontrollimine toimub käitusajal, lisades jälgimispunktidele töötlejad, mis kontrollivad täitmise tegelikku edenemist automaati etteantud võrdlusdeterministliku mudeli alusel, mis määratleb süsteemi eeldatava käitumise.
Jäljepunktidest pärinev teave liigutab mudeli ühest olekust teise ja kui uus olek ei vasta mudeli parameetritele, genereeritakse hoiatus või kernel asetatakse "paanikasse" (kõrge töökindlusega süsteemid peaksid tuvastama ja sellistele olukordadele reageerida). Automaadimudel, mis määratleb üleminekud ühest olekust teise, eksporditakse “dot” vormingusse (graphviz), misjärel tõlgitakse see dot2c utiliidi abil C-esitusse, mis laaditakse kerneli moodulina, mis jälgib täitmise edenemise kõrvalekaldeid eelmääratletud mudelist.
Käitusaegne mudelikontroll on kergem ja hõlpsamini rakendatav meetod missioonikriitiliste süsteemide õige täitmise kontrollimiseks, mis täiendab klassikalisi usaldusväärsuse kontrollimise meetodeid, nagu mudelikontroll ja koodi vastavuse matemaatilised tõendid ametlikus spetsifikatsioonidele. keel. RV eeliste hulgas on võime pakkuda ranget kontrolli ilma kogu süsteemi eraldi juurutamata modelleerimiskeeles, samuti paindlikku reageerimist ettenägematutele sündmustele, näiteks tõkestada kriitilistes süsteemides rikke edasist levikut.
Allikas: opennet.ru