Om onderdeel te worden van de Linux-kernel 5.20 (mogelijk krijgt de branch nummer 6.0) is een set patches voorgesteld met de implementatie van het RV-mechanisme (Runtime Verification), dat middelen biedt voor het controleren van de correctheid van de werking in hoogbetrouwbare systemen, die gegarandeerd storingsvrij zijn. De controle vindt tijdens de uitvoering plaats door handlers aan de traceerpunten te hechten, die de feitelijke uitvoering vergelijken met een vooraf gedefinieerd referentiemodel van een automaat, dat het verwachte gedrag van het systeem bepaalt.
Gegevens van de traceerpunten vertalen het model van de ene toestand naar de andere, en als de nieuwe toestand niet overeenkomt met de parameters van het model, wordt een waarschuwing gegenereerd of de kernel wordt in de staat 'panic' gebracht (er wordt verondersteld dat hoogbetrouwbare systemen dergelijke situaties detecteren en erop reageren). Het automaatmodel, dat de overgangen van de ene toestand naar de andere bepaalt, wordt geƫxporteerd in het 'dot'-formaat (graphviz), waarna het wordt getransformeerd met behulp van de utility dot2c naar een representatie in de programmeertaal C, die wordt geladen in de vorm van een kernelmodule die afwijkingen van de vooraf gedefinieerde modeluitvoering volgt.
De controle met het model tijdens de uitvoering wordt gepositioneerd als een lichtere en eenvoudigere manier om de correctheid van de uitvoering in kritieke systemen te bevestigen, ter aanvulling op de klassieke methoden voor betrouwbaarheid bevestiging, zoals modelcontrole en wiskundige bewijzen van de overeenstemming van de code met de specificaties die zijn vastgesteld in een formele taal. Tot de voordelen van RV behoort de mogelijkheid om strikte verificatie te bieden zonder een aparte implementatie van het gehele systeem in de modelleertaal, evenals flexibele reacties op onvoorziene gebeurtenissen, bijvoorbeeld om verdere verspreiding van storingen in kritieke systemen te blokkeren.
Bron: opennet.ru
