Per l'inclusione nel kernel Linux 5.20 (è possibile che il ramo assuma il numero 6.0), è stato proposto un insieme di patch che implementano il meccanismo RV (Runtime Verification), che fornisce strumenti per verificare la correttezza operativa in sistemi ad alta affidabilità, garantendo l'assenza di guasti. La verifica avviene durante l'esecuzione attraverso l'aggancio di gestori ai punti di tracciamento, confrontando il percorso effettivo di esecuzione con un modello deterministico di riferimento predefinito, che definisce il comportamento atteso del sistema.
Le informazioni dai punti di tracciamento traducono il modello da uno stato all'altro e, se il nuovo stato non corrisponde ai parametri del modello, viene generato un avviso o il kernel viene portato nello stato di 'panic' (si presume che i sistemi ad alta affidabilità definiscano tali situazioni e reagiscano di conseguenza). Il modello dell'automa, che definisce le transizioni da uno stato all'altro, viene esportato in formato 'dot' (graphviz), quindi tradotto tramite lo strumento dot2c in una rappresentazione in linguaggio C, che viene caricato come modulo del kernel e monitora le deviazioni del percorso di esecuzione rispetto al modello predefinito.
La verifica con il modello durante l'esecuzione è posizionata come un metodo più leggero e semplice da implementare nella pratica per confermare la correttezza operativa in sistemi critici, integrando i metodi classici di verifica della affidabilità, come la verifica del modello e le dimostrazioni matematiche di conformità del codice alle specifiche definite in linguaggio formale. Tra i vantaggi dell'RV si evidenzia la possibilità di garantire una rigorosa verifica senza necessità di una implementazione completa dell'intero sistema in linguaggio di modellazione, nonché una risposta flessibile a eventi imprevisti, ad esempio per bloccare la diffusione di guasti in sistemi critici.
Fonte: opennet.ru
