Per a Linux, s'ha proposat un mecanisme per verificar el correcte funcionament del nucli

Per a la seva inclusió en el nucli de Linux 5.20 (potser la branca tindrà la numeració 6.0), es proposa un conjunt de pedaços amb la implementació del mecanisme RV (Runtime Verification), que proporciona eines per comprovar el correcte funcionament en sistemes altament fiables que garanteixen el absència de fallades. La verificació es realitza en temps d'execució mitjançant l'adhesió de controladors a punts de traça que comproven el progrés real de l'execució amb un model determinista de referència predeterminat de l'autòmat que defineix el comportament esperat del sistema.

La informació dels punts de traça mou el model d'un estat a un altre, i si el nou estat no coincideix amb els paràmetres del model, es genera un avís o el nucli es col·loca en un estat de "pànic" (s'espera que els sistemes d'alta fiabilitat detectin i respondre a aquestes situacions). El model d'autòmat, que defineix les transicions d'un estat a un altre, s'exporta al format "punt" (graphviz), després del qual es tradueix mitjançant la utilitat dot2c a una representació C, que es carrega en forma d'un mòdul del nucli que fa un seguiment de les desviacions del progrés d'execució respecte al model predefinit.

Per a Linux, s'ha proposat un mecanisme per verificar el correcte funcionament del nucli

La verificació de models en temps d'execució es posiciona com un mètode més lleuger i més fàcil d'implementar per verificar l'execució correcta en sistemes de missió crítica, complementant els mètodes clàssics de verificació de la fiabilitat, com ara la verificació de models i les proves matemàtiques del compliment del codi amb les especificacions donades en forma formal. llenguatge. Entre els avantatges de RV hi ha la capacitat de proporcionar una verificació estricta sense una implementació separada de tot el sistema en un llenguatge de modelatge, així com una resposta flexible a esdeveniments imprevistos, per exemple, per bloquejar la propagació posterior d'una fallada en sistemes crítics.

Font: opennet.ru

Afegeix comentari