Fyrir Linux hefur verið lagt til kerfi til að sannreyna rétta virkni kjarnans

Til að vera með í Linux kjarna 5.20 (kannski verður útibúið númer 6.0) er lagt til sett af plástra með útfærslu RV (Runtime Verification) vélbúnaðarins, sem veitir verkfæri til að athuga rétta virkni á mjög áreiðanlegum kerfum sem tryggja skortur á mistökum. Staðfesting er framkvæmd á keyrslutíma með því að tengja meðhöndlunarstaði við rakningarpunkta sem athuga raunverulega framvindu framkvæmdar á móti fyrirfram ákveðnu viðmiðunardeterministic líkani sjálfvirkans sem skilgreinir væntanlega hegðun kerfisins.

Upplýsingar frá rekjapunktum flytja líkanið úr einu ástandi í annað og ef nýja ástandið passar ekki við færibreytur líkansins, myndast viðvörun eða kjarninn er settur í „panic“ ástand (vænt er að kerfi með mikla áreiðanleika greini og bregðast við slíkum aðstæðum). Sjálfvirka líkanið, sem skilgreinir umskipti frá einu ástandi í annað, er flutt út á „punkta“ sniðið (graphviz), eftir það er það þýtt með því að nota dot2c tólið yfir í C ​​framsetningu, sem er hlaðið í formi kjarnaeiningu sem fylgist með frávikum framkvæmdarframvindu frá fyrirfram skilgreindu líkani.

Fyrir Linux hefur verið lagt til kerfi til að sannreyna rétta virkni kjarnans

Módelathugun á keyrslutíma er staðsett sem léttari og auðveldari í framkvæmd aðferð til að sannreyna rétta framkvæmd á mikilvægum kerfum, sem viðbót við klassískar áreiðanleikasannprófunaraðferðir eins og módelathugun og stærðfræðilegar sannanir um samræmi við kóða við forskriftir sem gefnar eru í formlegu kerfi. tungumál. Meðal kosta RV er hæfileikinn til að veita stranga sannprófun án sérstakrar útfærslu á öllu kerfinu á líkanamáli, sem og sveigjanleg viðbrögð við ófyrirséðum atburðum, til dæmis til að hindra frekari útbreiðslu bilunar í mikilvægum kerfum.

Heimild: opennet.ru

Bæta við athugasemd