Per l'inclusione nel kernel Linux 5.20 (forse il ramo avrà la numerazione 6.0), viene proposto un set di patch con l'implementazione del meccanismo RV (Runtime Verification), che fornisce strumenti per la verifica del corretto funzionamento su sistemi altamente affidabili che garantiscono la assenza di fallimenti. La verifica viene eseguita in fase di esecuzione collegando gestori a punti di traccia che controllano l'effettivo progresso dell'esecuzione rispetto a un modello deterministico di riferimento predeterminato dell'automa che definisce il comportamento previsto del sistema.
Le informazioni provenienti dai punti di tracciamento spostano il modello da uno stato a un altro e, se il nuovo stato non corrisponde ai parametri del modello, viene generato un avviso o il kernel viene posto in uno stato di "panico" (si prevede che i sistemi ad alta affidabilità rilevino e rispondere a tali situazioni). Il modello dell'automa, che definisce le transizioni da uno stato all'altro, viene esportato nel formato "punto" (graphviz), dopodiché viene tradotto utilizzando l'utilità dot2c in una rappresentazione C, che viene caricata sotto forma di un modulo del kernel che tiene traccia delle deviazioni dell'avanzamento dell'esecuzione rispetto al modello predefinito.
Il controllo del modello in fase di esecuzione si posiziona come un metodo più leggero e più facile da implementare per verificare la corretta esecuzione su sistemi mission-critical, integrando i metodi classici di verifica dell'affidabilità come il controllo del modello e le prove matematiche della conformità del codice con le specifiche fornite in un documento formale. lingua. Tra i vantaggi di RV c'è la capacità di fornire una verifica rigorosa senza un'implementazione separata dell'intero sistema in un linguaggio di modellazione, nonché una risposta flessibile a eventi imprevisti, ad esempio, per bloccare l'ulteriore propagazione di un guasto nei sistemi critici.
Fonte: opennet.ru