Za Linux je bil predlagan mehanizem za preverjanje pravilnega delovanja jedra

Za vključitev v jedro Linuxa 5.20 (morda bo veja označena s številko 6.0) je predlagan komplet popravkov z implementacijo mehanizma RV (Runtime Verification), ki zagotavlja orodja za preverjanje pravilnega delovanja na zelo zanesljivih sistemih, ki zagotavljajo odsotnost napak. Preverjanje se izvaja v času izvajanja s pripenjanjem upravljavcev na točke sledenja, ki preverjajo dejanski napredek izvajanja glede na vnaprej določen referenčni deterministični model avtomata, ki definira pričakovano vedenje sistema.

Informacije iz točk sledenja premaknejo model iz enega stanja v drugo in če se novo stanje ne ujema s parametri modela, se ustvari opozorilo ali pa se jedro postavi v stanje "panike" (pričakuje se, da sistemi z visoko zanesljivostjo zaznajo in se odzvati na takšne situacije). Model avtomata, ki definira prehode iz enega stanja v drugo, se izvozi v format “dot” (graphviz), nakar se s pripomočkom dot2c prevede v predstavitev C, ki se naloži v obliki modula jedra, ki sledi odstopanjem napredka izvajanja od vnaprej določenega modela.

Za Linux je bil predlagan mehanizem za preverjanje pravilnega delovanja jedra

Preverjanje modela med izvajanjem je postavljeno kot lažja in enostavnejša za implementacijo metoda preverjanja pravilne izvedbe na kritičnih sistemih, ki dopolnjuje klasične metode preverjanja zanesljivosti, kot so preverjanje modela in matematični dokazi o skladnosti kode s specifikacijami, podanimi v formalnem jezik. Med prednostmi RV je zmožnost zagotavljanja strogega preverjanja brez ločene implementacije celotnega sistema v modelnem jeziku, kot tudi prilagodljiv odziv na nepredvidene dogodke, na primer za blokiranje nadaljnjega širjenja napake v kritičnih sistemih.

Vir: opennet.ru

Dodaj komentar