For Linux er det foreslått en mekanisme for å verifisere korrekt drift av kjernen

For inkludering i Linux-kjernen 5.20 (kanskje grenen vil bli nummerert 6.0), foreslås et sett med oppdateringer med implementering av RV-mekanismen (Runtime Verification), som gir verktøy for å kontrollere riktig drift på svært pålitelige systemer som garanterer fravær av feil. Verifikasjon utføres ved kjøretid ved å knytte behandlere til sporingspunkter som kontrollerer den faktiske fremdriften av utførelse mot en forhåndsbestemt referanse deterministisk modell av automaten som definerer den forventede oppførselen til systemet.

Informasjon fra sporingspunkter flytter modellen fra en tilstand til en annen, og hvis den nye tilstanden ikke samsvarer med parametrene til modellen, genereres en advarsel eller kjernen settes i en "panikk"-tilstand (systemer med høy pålitelighet forventes å oppdage og reagere på slike situasjoner). Automatmodellen, som definerer overganger fra en tilstand til en annen, eksporteres til "dot"-formatet (graphviz), hvoretter den blir oversatt ved hjelp av dot2c-verktøyet til en C-representasjon, som lastes inn i form av en kjernemodul som sporer avvik i utførelsesfremdriften fra den forhåndsdefinerte modellen.

For Linux er det foreslått en mekanisme for å verifisere korrekt drift av kjernen

Kjøretidsmodellkontroll er posisjonert som en lettere og enklere å implementere metode for å verifisere korrekt utførelse på oppdragskritiske systemer, som komplementerer klassiske pålitelighetsverifiseringsmetoder som modellsjekking og matematiske bevis på kodesamsvar med spesifikasjoner gitt i en formell Språk. Blant fordelene med RV er muligheten til å gi streng verifisering uten en separat implementering av hele systemet i et modelleringsspråk, samt fleksibel respons på uforutsette hendelser, for eksempel for å blokkere videre spredning av en feil i kritiske systemer.

Kilde: opennet.ru

Legg til en kommentar