Za uključivanje u Linux kernel 5.20 (možda će grana biti označena brojem 6.0), predložen je set zakrpa sa implementacijom RV (Runtime Verification) mehanizma, koji pruža alate za provjeru ispravnog rada na visoko pouzdanim sistemima koji garantuju odsustvo kvarova. Provjera se izvodi u vrijeme izvođenja pričvršćivanjem rukovalaca na tačke praćenja koje provjeravaju stvarni napredak izvršenja u odnosu na unaprijed određeni referentni deterministički model automata koji definira očekivano ponašanje sistema.
Informacije iz tačaka traga pomiču model iz jednog stanja u drugo, a ako novo stanje ne odgovara parametrima modela, generira se upozorenje ili se kernel stavlja u "panično" stanje (očekuje se da će sistemi visoke pouzdanosti otkriti i reagovati na takve situacije). Model automata, koji definiše prelaze iz jednog stanja u drugo, eksportuje se u „tačkasti“ format (graphviz), nakon čega se prevodi pomoću dot2c uslužnog programa u C reprezentaciju, koja se učitava u obliku modula kernela koji prati odstupanja napredovanja izvršenja od unapred definisanog modela.
Provjera modela tokom izvođenja pozicionirana je kao lakša i lakša za implementaciju metoda provjere ispravnog izvršenja na sistemima od ključne važnosti, dopunjujući klasične metode verifikacije pouzdanosti kao što su provjera modela i matematički dokazi usklađenosti koda sa specifikacijama datim u formalnom obliku. jezik. Među prednostima RV-a je i mogućnost da se obezbedi stroga verifikacija bez odvojene implementacije celog sistema u jeziku modeliranja, kao i fleksibilan odgovor na nepredviđene događaje, na primer, da se blokira dalje širenje kvara u kritičnim sistemima.
izvor: opennet.ru