Voor opname in de Linux-kernel 5.20 (misschien krijgt de branch nummer 6.0) wordt een reeks patches voorgesteld met de implementatie van het RV-mechanisme (Runtime Verification), dat hulpmiddelen biedt voor het controleren van de juiste werking op zeer betrouwbare systemen die de afwezigheid van mislukkingen. Verificatie wordt tijdens runtime uitgevoerd door handlers aan traceerpunten te koppelen die de feitelijke voortgang van de uitvoering controleren aan de hand van een vooraf bepaald referentiedeterministisch model van de automaat dat het verwachte gedrag van het systeem definieert.
Informatie van traceerpunten verplaatst het model van de ene toestand naar de andere, en als de nieuwe toestand niet overeenkomt met de parameters van het model, wordt er een waarschuwing gegenereerd of wordt de kernel in een ‘paniek’-toestand gebracht (systemen met een hoge betrouwbaarheid zullen naar verwachting en reageren op dergelijke situaties). Het automaatmodel, dat overgangen van de ene toestand naar de andere definieert, wordt geëxporteerd naar het “dot”-formaat (graphviz), waarna het met behulp van het dot2c-hulpprogramma wordt vertaald naar een C-representatie, die wordt geladen in de vorm van een kernelmodule die houdt afwijkingen bij van de voortgang van de uitvoering ten opzichte van het vooraf gedefinieerde model.
Runtimemodelcontrole wordt gepositioneerd als een lichtere en gemakkelijker te implementeren methode voor het verifiëren van de juiste uitvoering op bedrijfskritische systemen, als aanvulling op klassieke methoden voor betrouwbaarheidsverificatie, zoals modelcontrole en wiskundige bewijzen van code-conformiteit met specificaties die in een formeel document zijn vastgelegd. taal. Een van de voordelen van RV is de mogelijkheid om strikte verificatie te bieden zonder een afzonderlijke implementatie van het hele systeem in een modelleringstaal, evenals een flexibele reactie op onvoorziene gebeurtenissen, bijvoorbeeld om de verdere verspreiding van een storing in kritieke systemen te blokkeren.
Bron: opennet.ru