{"id":104790,"date":"2022-08-07T21:36:50","date_gmt":"2022-08-07T19:36:51","guid":{"rendered":"https:\/\/prohoster.info\/blog\/novosti-interneta\/dlya-linux-predlozhen-mehanizm-verifikaczii-korrektnosti-raboty-yadra"},"modified":"2022-08-07T21:36:50","modified_gmt":"2022-08-07T19:36:51","slug":"dlya-linux-predlozhen-mehanizm-verifikaczii-korrektnosti-raboty-yadra","status":"publish","type":"post","link":"https:\/\/prohoster.info\/nl\/blog\/news\/dlya-linux-predlozhen-mehanizm-verifikaczii-korrektnosti-raboty-yadra","title":{"rendered":"Er is een mechanisme voor de verificatie van de correcte werking van de Linux-kernel voorgesteld","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"
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. <\/p>\n
Informatie van tracepunten vertaalt het model van de ene staat naar de andere, en als de nieuwe staat niet overeenkomt met de parameters van het model, wordt er een waarschuwing gegenereerd of wordt de kernel in de staat 'panic' gebracht (veronderstelt dat zeer betrouwbare systemen dergelijke situaties zullen detecteren en erop reageren). Het automaatmodel dat de overgangen van de ene staat naar de andere definieert, wordt ge\u00ebxporteerd naar het 'dot' (graphviz) formaat, waarna het wordt getransformeerd met behulp van de tool dot2c naar een voorstelling in de programmeertaal C, die wordt geladen in de vorm van een kernelmodule die afwijkingen van de gedefinieerde modeluitvoering volgt.
<\/center> <\/p>\n
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. \n Bron: opennet.ru<\/a> <\/p>","protected":false,"gt_translate_keys":[{"key":"rendered","format":"html"}]},"excerpt":{"rendered":"
![\"Er](\"\/wp-content\/uploads\/2022\/08\/56f02964c804a17b5cf5d811b2777368.jpg\")
<\/center> <\/p>\n