Linux 5.20 tuumisse on ettepanek teha rida patšosid RV (Runtime Verification) mehhanismi rakendamiseks, mis on mõeldud kõrge töökindluse süsteemide nõuetekohase toimimise kontrollimiseks, tagades katkestuste puudumise. Kontrollimine toimub töö ajal, liites töötlejad jälgimispunktidele, mis võrreldavad tegelikku teostust eelnevalt määratletud etalondeterministliku automaadi mudeliga, millel on määratud süsteemi oodatav käitumine.
Jälgimispunktid edastavad teabe mudeli üleminekust ühest olekust teise ning kui uus olek ei vasta mudeli parameetritele, genereeritakse hoiatus või südamik viidatakse 'panic' olekusse (eeldatakse, et kõrge usaldusväärsusega süsteemid tuvastavad sellised olukorrad ja reageerivad neile). Automatiseeritud mudel, mis määratleb üleminekud ühest olekust teise, eksporditakse 'dot' (graphviz) formaati, seejärel tõlgitakse see kasutades utiliiti dot2c C keele esitusena, mis laaditakse südamiku moodulina, jälgides täitmise kõrvalekaldeid ettenähtud mudelist.
Mudeli käitlemine töö ajal peetakse kergemaks ja lihtsamaks viisiks süsteemide korrektsuse tõendamiseks kriitilistes valdkondades, täiustades klassikalisi usaldusväärsuse kinnitamise meetodeid, nagu mudeli kontrollimine ja matemaatilised tõendid koodi vastavuse kohta määratud spetsiifikale formaalses keeles. RV eeliste hulka kuulub võimalus tagada ranget verifitseerimist ilma, et oleks vaja kogu süsteemi eraldi modelleerimise keeles teostada, ning paindlik reageerimine ettenägematutele olukordadele, näiteks kriitilistes süsteemides edasise rikke leviku peatamine.
Allikas: opennet.ru
