Na začlenenie do jadra Linux 5.20 (je možné, že vetva získa číslo 6.0) bol navrhnutý súbor záplat s implementáciou mechanizmu RV (Runtime Verification), ktorý predstavuje prostriedky na kontrolu správnosti fungovania na vysoko spoľahlivých systémoch, zaručujúcich absenciu výpadkov. Kontrola sa vykonáva počas vykonávania prostredníctvom pripojenia spracovateľov k miestam sledovania, ktoré porovnávajú skutočný priebeh vykonávania s vopred určeným referenčným deterministickým modelom automatu, určujúcim očakávané správanie systému.
Informácie z miest sledovania prevádzajú model z jedného stavu do druhého, a ak nový stav nezodpovedá parametrom modelu, generuje sa varovanie alebo jadro sa prevádza do stavu 'panic' (predpokladá sa, že vysoko spoľahlivé systémy budú určovať takéto situácie a reagovať na ne). Model automatu, ktorý určuje prechody z jedného stavu do druhého, sa exportuje do formátu 'dot' (graphviz), a potom sa translituje pomocou utilitky dot2c do reprezentácie v jazyku C, ktorá sa načíta vo forme modulu jadra, sledujúceho odchýlky vykonávania od vopred určeného modelu.
Porovnanie s modelom počas vykonávania sa pozicionuje ako ľahší a jednoduchší spôsob potvrdenia správnosti vykonávania na kriticky dôležitých systémoch, dopĺňajúci klasické metódy potvrdenia spoľahlivosti, ako je kontrola modelu a matematické dôkazy súladu kódu so špecifikáciami, stanovenými v formálnom jazyku. Medzi výhody RV patrí možnosť zabezpečiť prísnu verifikáciu bez zvláštnej implementácie celého systému v jazyku modelovania, ako aj flexibilné reagovanie na nepredvídané udalosti, napríklad na blokovanie ďalšieho šírenia výpadku v kriticky dôležitých systémoch.
Zdroj: opennet.ru
