Operētājsistēmai Linux ir piedāvāts mehānisms, lai pārbaudītu kodola pareizu darbību

Lai iekļautu Linux kodolā 5.20 (iespējams, filiāle tiks numurēta ar 6.0), tiek piedāvāts ielāpu komplekts ar RV (Runtime Verification) mehānisma ieviešanu, kas nodrošina rīkus pareizas darbības pārbaudei ļoti uzticamās sistēmās, kas garantē neveiksmju trūkums. Verifikācija tiek veikta izpildes laikā, pievienojot apdarinātājus izsekošanas punktiem, kas pārbauda faktisko izpildes gaitu, salīdzinot ar iepriekš noteiktu automāta atsauces deterministisko modeli, kas nosaka paredzamo sistēmas uzvedību.

Informācija no izsekošanas punktiem pārvieto modeli no viena stāvokļa uz citu, un, ja jaunais stāvoklis neatbilst modeļa parametriem, tiek ģenerēts brīdinājums vai kodols tiek novietots "panikas" stāvoklī (paredzams, ka sistēmas ar augstu uzticamību to noteiks un reaģēt uz šādām situācijām). Automāta modelis, kas definē pārejas no viena stāvokļa uz citu, tiek eksportēts uz “dot” formātu (graphviz), pēc kura tas, izmantojot dot2c utilītu, tiek pārtulkots C attēlojumā, kas tiek ielādēts kodola moduļa formā, izseko izpildes progresa novirzes no iepriekš definētā modeļa.

Operētājsistēmai Linux ir piedāvāts mehānisms, lai pārbaudītu kodola pareizu darbību

Modeļa izpildlaika pārbaude tiek pozicionēta kā vieglāka un vieglāk ieviešama metode, lai pārbaudītu pareizu izpildi misijai kritiskās sistēmās, kas papildina klasiskās uzticamības pārbaudes metodes, piemēram, modeļa pārbaudi un matemātiskos pierādījumus par koda atbilstību formālajām specifikācijām. valodu. Starp RV priekšrocībām ir iespēja nodrošināt stingru verifikāciju bez atsevišķas visas sistēmas ieviešanas modelēšanas valodā, kā arī elastīgu reakciju uz neparedzētiem notikumiem, piemēram, bloķēt tālāku kļūmes izplatīšanos kritiskajās sistēmās.

Avots: opennet.ru

Pievieno komentāru