Pro začlenění do linuxového jádra 5.20 (možná bude mít větev číslo 6.0) je navržena sada záplat s implementací mechanismu RV (Runtime Verification), který poskytuje nástroje pro kontrolu správného fungování na vysoce spolehlivých systémech zaručujících absence poruch. Ověření se provádí za běhu připojením obslužných rutin ke trasovacím bodům, které kontrolují skutečný průběh provádění oproti předem určenému referenčnímu deterministickému modelu automatu, který definuje očekávané chování systému.
Informace ze sledovacích bodů posouvají model z jednoho stavu do druhého, a pokud nový stav neodpovídá parametrům modelu, vygeneruje se varování nebo se jádro dostane do „panického“ stavu (očekává se, že systémy s vysokou spolehlivostí detekují a reagovat na takové situace). Model automatu, který definuje přechody z jednoho stavu do druhého, je exportován do formátu „tečka“ (graphviz), načež je přeložen pomocí utility dot2c do reprezentace C, která je načtena ve formě modulu jádra, který sleduje odchylky postupu provádění od předdefinovaného modelu.
Kontrola modelu za běhu je umístěna jako lehčí a snáze implementovatelná metoda ověřování správného provádění na kritických systémech, která doplňuje klasické metody ověřování spolehlivosti, jako je kontrola modelu a matematické důkazy souladu kódu se specifikacemi uvedenými ve formálním Jazyk. Mezi výhody RV patří schopnost zajistit přísnou verifikaci bez samostatné implementace celého systému v modelovacím jazyce a také flexibilní reakce na nepředvídané události, například blokování dalšího šíření poruchy v kritických systémech.
Zdroj: opennet.ru