For Linux foreslås en mekanisme til at verificere korrektheden af ​​kernen

For at blive inkluderet i Linux 5.20-kernen (måske grenen bliver nummereret 6.0), er et sæt patches blevet foreslået med implementeringen af ​​RV-mekanismen (Runtime Verification), som er et middel til at kontrollere den korrekte drift på yderst pålidelige systemer der garanterer fravær af fejl. Validering udføres ved kørsel ved at knytte handlere til sporingspunkter, der kontrollerer den faktiske fremdrift af eksekveringen mod en forudbestemt reference deterministisk model af automaten, der bestemmer systemets forventede opførsel.

Information fra sporpunkter flytter modellen fra en tilstand til en anden, og hvis den nye tilstand ikke matcher modellens parametre, genereres en advarsel, eller kernen sættes i en "panik"-tilstand (det er underforstået, at meget pålidelige systemer vil opdage sådanne situationer og reagere på dem). Automatmodellen, der definerer overgange fra en tilstand til en anden, eksporteres til "dot" (graphviz) formatet, hvorefter den oversættes ved hjælp af dot2c-værktøjet til en C-repræsentation, som indlæses i form af et kernemodul, der sporer afvigelser af eksekveringsforløbet fra en foruddefineret model.

For Linux foreslås en mekanisme til at verificere korrektheden af ​​kernen

Kørselsmodelkontrol er placeret som en mere let og nem at implementere metode til at verificere korrektheden af ​​udførelsen på missionskritiske systemer, som komplementerer klassiske metoder til pålidelighedsverifikation, såsom modelkontrol og matematiske beviser for kodeoverholdelse med givne specifikationer i et formelt sprog. Blandt fordelene ved RV er muligheden for at levere streng verifikation uden en separat implementering af hele systemet i et modelleringssprog, samt en fleksibel reaktion på uforudsete hændelser, for eksempel for at blokere for yderligere udbredelse af en fejl i kritiske systemer.

Kilde: opennet.ru

Tilføj en kommentar