Për Linux, një mekanizëm është propozuar për të verifikuar funksionimin e saktë të kernelit

Për përfshirje në kernelin Linux 5.20 (ndoshta dega do të numërohet 6.0), propozohet një grup arnimesh me zbatimin e mekanizmit RV (Runtime Verification), i cili ofron mjete për të kontrolluar funksionimin e saktë në sisteme shumë të besueshme që garantojnë mungesa e dështimeve. Verifikimi kryhet në kohën e ekzekutimit duke i bashkangjitur mbajtësit në pikat e gjurmimit që kontrollojnë progresin aktual të ekzekutimit kundrejt një modeli të paracaktuar referimi përcaktues të automatit që përcakton sjelljen e pritur të sistemit.

Informacioni nga pikat e gjurmës e zhvendos modelin nga një gjendje në tjetrën dhe nëse gjendja e re nuk përputhet me parametrat e modelit, gjenerohet një paralajmërim ose kerneli vendoset në gjendje "paniku" (sistemet me besueshmëri të lartë pritet të zbulojnë dhe reagoni në situata të tilla). Modeli i automatit, i cili përcakton kalimet nga një gjendje në tjetrën, eksportohet në formatin "dot" (graphviz), pas së cilës përkthehet duke përdorur mjetin dot2c në një paraqitje C, e cila ngarkohet në formën e një moduli kernel që gjurmon devijimet e progresit të ekzekutimit nga modeli i paracaktuar.

Për Linux, një mekanizëm është propozuar për të verifikuar funksionimin e saktë të kernelit

Kontrolli i modelit në kohë ekzekutimi pozicionohet si një metodë më e lehtë dhe më e lehtë për t'u zbatuar për verifikimin e ekzekutimit të saktë në sistemet kritike të misionit, duke plotësuar metodat klasike të verifikimit të besueshmërisë si kontrolli i modelit dhe provat matematikore të përputhshmërisë së kodit me specifikimet e dhëna në një zyrtar gjuhe. Ndër avantazhet e RV është aftësia për të siguruar verifikim të rreptë pa një zbatim të veçantë të të gjithë sistemit në një gjuhë modelimi, si dhe përgjigje fleksibël ndaj ngjarjeve të paparashikuara, për shembull, për të bllokuar përhapjen e mëtejshme të një dështimi në sistemet kritike.

Burimi: opennet.ru

Shto një koment