För Linux har en mekanism föreslagits för att verifiera att kärnan fungerar korrekt

För inkludering i Linux-kärnan 5.20 (kanske grenen kommer att vara numrerad 6.0) föreslås en uppsättning patchar med implementeringen av RV-mekanismen (Runtime Verification), som tillhandahåller verktyg för att kontrollera korrekt funktion på mycket tillförlitliga system som garanterar frånvaro av misslyckanden. Verifiering utförs vid körning genom att koppla hanterare till spårningspunkter som kontrollerar det faktiska framstegen i exekveringen mot en förutbestämd referens deterministisk modell av automaten som definierar systemets förväntade beteende.

Information från spårpunkter flyttar modellen från ett tillstånd till ett annat, och om det nya tillståndet inte matchar modellens parametrar genereras en varning eller så placeras kärnan i ett "panik"-tillstånd (system med hög tillförlitlighet förväntas upptäcka och reagera på sådana situationer). Automatmodellen, som definierar övergångar från ett tillstånd till ett annat, exporteras till "dot"-formatet (graphviz), varefter den översätts med hjälp av dot2c-verktyget till en C-representation, som laddas i form av en kärnmodul som spårar avvikelser i exekveringsförloppet från den fördefinierade modellen.

För Linux har en mekanism föreslagits för att verifiera att kärnan fungerar korrekt

Körtidsmodellkontroll är placerad som en lättare och enklare att implementera metod för att verifiera korrekt exekvering på verksamhetskritiska system, som kompletterar klassiska metoder för tillförlitlighetsverifiering som modellkontroll och matematiska bevis för kodöverensstämmelse med specifikationer som ges i en formell språk. Bland fördelarna med RV är möjligheten att tillhandahålla strikt verifiering utan en separat implementering av hela systemet i ett modelleringsspråk, samt flexibel respons på oförutsedda händelser, till exempel för att blockera vidare spridning av ett fel i kritiska system.

Källa: opennet.ru

Lägg en kommentar