Linux-ի համար առաջարկվել է մեխանիզմ՝ ստուգելու միջուկի ճիշտ աշխատանքը

Linux-ի միջուկում 5.20-ում ներառելու համար (հնարավոր է, որ մասնաճյուղը համարակալվի 6.0), առաջարկվում է մի շարք patches՝ RV (Runtime Verification) մեխանիզմի ներդրմամբ, որն ապահովում է գործիքներ՝ բարձր հուսալի համակարգերի վրա ճիշտ աշխատանքը ստուգելու համար, որոնք երաշխավորում են ձախողումների բացակայություն. Ստուգումն իրականացվում է գործարկման ժամանակ՝ կարգավորիչները կցելով հետագծային կետերին, որոնք ստուգում են կատարման իրական առաջընթացը ավտոմատի կանխորոշված ​​դետերմինիստական ​​մոդելի համեմատ, որը սահմանում է համակարգի սպասվող վարքագիծը:

Հետագծային կետերից ստացված տեղեկատվությունը մոդելը տեղափոխում է մի վիճակից մյուսը, և եթե նոր վիճակը չի համապատասխանում մոդելի պարամետրերին, ստեղծվում է նախազգուշացում կամ միջուկը տեղադրվում է «խուճապային» վիճակում (ակնկալվում է, որ բարձր հուսալիության համակարգերը կհայտնաբերեն և արձագանքել նման իրավիճակներին): Ավտոմատ մոդելը, որը սահմանում է անցումները մի վիճակից մյուսը, արտահանվում է «կետ» ձևաչափով (graphviz), որից հետո այն թարգմանվում է dot2c ծրագրի միջոցով C ներկայացման, որը բեռնվում է միջուկի մոդուլի տեսքով, որը հետևում է կատարման առաջընթացի շեղումները նախապես սահմանված մոդելից:

Linux-ի համար առաջարկվել է մեխանիզմ՝ ստուգելու միջուկի ճիշտ աշխատանքը

Գործարկման ժամանակի մոդելի ստուգումը դիրքավորվում է որպես առաքելության կարևոր համակարգերում ճիշտ կատարումը ստուգելու ավելի թեթև և ավելի հեշտ իրագործելի մեթոդ, որը լրացնում է հուսալիության ստուգման դասական մեթոդները, ինչպիսիք են մոդելի ստուգումը և կոդերի համապատասխանության մաթեմատիկական ապացույցները, որոնք տրված են պաշտոնական փաստաթղթում: լեզու. RV-ի առավելությունների թվում է խիստ ստուգում ապահովելու հնարավորությունը՝ առանց ամբողջ համակարգի առանձին ներդրման մոդելավորման լեզվով, ինչպես նաև անկանխատեսելի իրադարձություններին ճկուն արձագանքելու հնարավորություն, օրինակ՝ արգելափակելու ձախողման հետագա տարածումը կրիտիկական համակարգերում:

Source: opennet.ru

Добавить комментарий