Per l'inclusione nel kernel Linux 5.20 (è possibile che il ramo riceva il numero 6.0) è stato proposto un insieme di patch con l'implementazione del meccanismo RV (Runtime Verification), che rappresenta strumenti per verificare la correttezza del funzionamento su sistemi ad alta affidabilità, garantendo l'assenza di guasti. La verifica avviene durante l'esecuzione tramite l'allegato di gestori ai punti di tracciamento, che confrontano il corso effettivo dell'esecuzione con un modello deterministico di riferimento precedentemente definito, che determina 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 presuppone che i sistemi ad alta affidabilità possano identificare tali situazioni e reagire di conseguenza). Il modello del automata, che definisce le transizioni da uno stato all'altro, è esportato in formato «dot» (graphviz), e poi tradotto con l'utility dot2c in una rappresentazione in linguaggio C, che viene caricata come modulo del kernel, monitorando le deviazioni dell'esecuzione dal modello predeterminato.
Il confronto con il modello durante l'esecuzione è posizionato come un modo più leggero e semplice da implementare nella pratica per confermare la correttezza dell'esecuzione su sistemi critici, complementando i metodi classici di conferma dell'affidabilità, come la verifica del modello e le prove matematiche di conformità del codice alle specifiche fornite in un linguaggio formale. Tra i vantaggi dell'RV si menziona la possibilità di garantire una rigorosa verifica senza la necessità di implementare l'intero sistema in un linguaggio di modellazione, così come una flessibile reazione a eventi imprevisti, ad esempio, per bloccare la propagazione di guasti in sistemi critici.
Fonte: opennet.ru
