Pro jádro Linux 5.20 (možná získá verzi 6.0) byl navržen soubor patchů, který implementuje mechanismus RV (Runtime Verification), což představuje prostředky pro ověřování správnosti provozu v vysoce spolehlivých systémech, zaručujících absence selhání. Ověřování se provádí během běhu prostřednictvím připojení zpracovatelů k bodům sledování, které porovnávají aktuální průběh vykonávání s předem definovaným referenčním deterministickým modelem automatu, který určuje očekávané chování systému.
Informace z bodů sledování převádí model z jednoho stavu do druhého a pokud nový stav neodpovídá parametrům modelu, generuje se varování nebo jádro se přepne do stavu „panic“ (předpokládá se, že vysoce spolehlivé systémy rozpoznají takové situace a reagují na ně). Model automatu, který určuje přechody z jednoho stavu do druhého, je exportován do formátu „dot“ (graphviz), a poté je přeložen pomocí nástroje dot2c do podoby v jazyce C, která je načítána ve formě jádrového modulu sledujícího odchylky v průběhu vykonávání od předem stanoveného modelu.
Porovnání s modelem během běhu je představováno jako lehčí a jednodušší způsob, jak potvrdit správnost vykonávání na kriticky důležitých systémech, doplňující klasické metody potvrzení spolehlivosti, jako jsou ověření modelu a matematické důkazy souladu kódu se specifikacemi zadanými ve formálním jazyce. Mezi výhody RV patří možnost zaručit přísné ověřování bez nutnosti samostatné implementace celého systému v modelovacím jazyce, stejně jako flexibilní reakce na nepředvídané události, například pro zablokování dalšího šíření selhání v kriticky důležitých systémech.
Zdroj: opennet.ru
