Linux 5.20 nukleoan sartzeko (agian adarra 6.0 zenbakiduna izango da), RV (Runtime Verification) mekanismoaren ezarpenarekin adabaki-multzo bat proposatzen da, eta sistema fidagarrienetan funtzionamendu zuzena egiaztatzeko tresnak eskaintzen ditu. hutsegiterik eza. Egiaztapena exekuzioan egiten da kudeatzaileak erantsiz exekuzioaren benetako aurrerapena egiaztatzen duten traza-puntuei, sistemaren espero den portaera definitzen duen automataren erreferentzia-eredu deterministiko aurrez zehaztu batekin.
Aztarna puntuen informazioak egoera batetik bestera mugitzen du eredua, eta egoera berria ereduaren parametroekin bat ez badator, abisua sortzen da edo nukleoa "izua" egoeran jartzen da (fidagarritasun handiko sistemek detektatzea espero da. eta horrelako egoerei erantzun). Egoera batetik besterako trantsizioak definitzen dituen automata-eredua "puntu" formatura (graphviz) esportatzen da, eta ondoren dot2c erabilgarritasuna erabiliz C irudikapen batera itzultzen da, kernel modulu moduan kargatzen dena. Aurrez definitutako ereduaren exekuzioaren aurrerapenaren desbideraketak egiten ditu.
Exekuzio-denboran ereduaren egiaztapena misio kritikoko sistemetan exekuzio zuzena egiaztatzeko metodo arinago eta inplementatzeko metodo gisa kokatzen da, fidagarritasuna egiaztatzeko metodo klasikoak osatuz, hala nola, ereduen egiaztapena eta kodea formala batean emandako zehaztapenak betetzen direlako froga matematikoak. hizkuntza. RV-ren abantailen artean, sistema osoa modelizazio-lengoaia batean inplementatu gabe egiaztapen zorrotza eskaintzeko gaitasuna dago, baita ustekabeko gertakariei erantzun malgua ere, adibidez, sistema kritikoetan hutsegite bat gehiago hedatzea blokeatzeko.
Iturria: opennet.ru