Per l'inclusione in u kernel Linux 5.20 (forse u ramu serà numeratu 6.0), un inseme di patch hè prupostu cù l'implementazione di u mecanismu RV (Runtime Verification), chì furnisce strumenti per verificà u funziunamentu currettu in sistemi altamente affidabili chì guarantisci u assenza di fallimenti. A verificazione hè realizata in runtime attachendu i gestori à i punti di traccia chì verificanu u prugressu attuale di l'esekzione contr'à un mudellu deterministicu di riferimentu predeterminatu di l'automatu chì definisce u cumpurtamentu previstu di u sistema.
L'infurmazioni da i punti di traccia move u mudellu da un statu à l'altru, è se u novu statu ùn currisponde à i paràmetri di u mudellu, un avvisu hè generatu o u kernel hè postu in un statu "panicu" (i sistemi d'alta affidabilità sò previsti per detectà). è risponde à tali situazioni). U mudellu di l'automatizazione, chì definisce e transizioni da un statu à l'altru, hè esportatu à u formatu "puntu" (graphviz), dopu chì hè traduttu cù l'utilità dot2c in una rapprisintazioni C, chì hè caricata in forma di un modulu di kernel chì traccia i deviazioni di u prugressu di l'esecuzione da u mudellu predefinitu.
A verificazione di u mudellu di run-time hè posizionata cum'è un metudu più ligeru è più faciule da implementà per verificà l'esekzione curretta nantu à i sistemi di missione critica, chì cumplementa i metudi classici di verificazione di affidabilità cum'è a verificazione di mudelli è e prove matematiche di a conformità di u codice cù e specificazioni date in forma formale. lingua. Trà i vantaghji di RV hè a capacità di furnisce una verificazione stretta senza una implementazione separata di tuttu u sistema in una lingua di modellazione, è ancu una risposta flexible à avvenimenti imprevisti, per esempiu, per bluccà a propagazione ulteriore di un fallimentu in sistemi critichi.
Source: opennet.ru