Za Linux je predložen mehanizam za provjeru ispravnog rada jezgre

Za uključivanje u Linux kernel 5.20 (možda će grana biti označena brojem 6.0), predlaže se skup zakrpa s implementacijom mehanizma RV (Runtime Verification) koji pruža alate za provjeru ispravnog rada na vrlo pouzdanim sustavima koji jamče odsustvo kvarova. Provjera se provodi tijekom izvođenja pripajanjem rukovatelja točkama praćenja koji provjeravaju stvarni napredak izvršenja prema unaprijed određenom referentnom determinističkom modelu automata koji definira očekivano ponašanje sustava.

Informacije iz točaka praćenja pomiču model iz jednog stanja u drugo, a ako novo stanje ne odgovara parametrima modela, generira se upozorenje ili se kernel stavlja u stanje "panike" (očekuje se da sustavi visoke pouzdanosti otkriju i reagirati na takve situacije). Model automata, koji definira prijelaze iz jednog stanja u drugo, eksportira se u “dot” format (graphviz), nakon čega se pomoću uslužnog programa dot2c prevodi u C reprezentaciju, koja se učitava u obliku kernel modula koji prati odstupanja napretka izvršenja od unaprijed definiranog modela.

Za Linux je predložen mehanizam za provjeru ispravnog rada jezgre

Provjera modela tijekom izvođenja pozicionirana je kao lakša i lakša za implementaciju metoda provjere ispravnog izvođenja na kritičnim sustavima, nadopunjujući klasične metode provjere pouzdanosti kao što su provjera modela i matematički dokazi usklađenosti koda sa specifikacijama danim u formalnom Jezik. Među prednostima RV-a je mogućnost pružanja stroge provjere bez posebne implementacije cijelog sustava u jeziku za modeliranje, kao i fleksibilan odgovor na nepredviđene događaje, na primjer, za blokiranje daljnjeg širenja kvara u kritičnim sustavima.

Izvor: opennet.ru

Dodajte komentar