Pentru includerea în kernel-ul Linux 5.20 (poate că ramura va fi numerotată 6.0), este propus un set de patch-uri cu implementarea mecanismului RV (Runtime Verification), care oferă instrumente pentru verificarea funcționării corecte pe sisteme extrem de fiabile care garantează absența eșecurilor. Verificarea se efectuează în timpul execuției prin atașarea handler-urilor la punctele de urmărire care verifică progresul real al execuției față de un model determinist de referință predeterminat al automatului care definește comportamentul așteptat al sistemului.
Informațiile din punctele de urmărire mută modelul dintr-o stare în alta, iar dacă noua stare nu se potrivește cu parametrii modelului, se generează un avertisment sau nucleul este plasat într-o stare de „panică” (se așteaptă ca sistemele de înaltă fiabilitate să detecteze și răspunde la astfel de situații). Modelul automat, care definește tranzițiile de la o stare la alta, este exportat în formatul „punct” (graphviz), după care este tradus folosind utilitarul dot2c într-o reprezentare C, care este încărcată sub forma unui modul kernel care urmărește abaterile progresului execuției față de modelul predefinit.
Verificarea modelului în timpul execuției este poziționată ca o metodă mai ușoară și mai ușor de implementat de verificare a execuției corecte pe sisteme critice pentru misiune, completând metodele clasice de verificare a fiabilității, cum ar fi verificarea modelului și dovezile matematice ale conformității codului cu specificațiile date într-o formă formală. limba. Printre avantajele RV se numără capacitatea de a oferi o verificare strictă fără o implementare separată a întregului sistem într-un limbaj de modelare, precum și un răspuns flexibil la evenimente neprevăzute, de exemplu, pentru a bloca propagarea ulterioară a unei defecțiuni în sistemele critice.
Sursa: opennet.ru