Linux အတွက်၊ kernel ၏ မှန်ကန်သောလုပ်ဆောင်ချက်ကို အတည်ပြုရန် ယန္တရားတစ်ခု အဆိုပြုထားသည်။

Linux kernel 5.20 (ဌာနခွဲကို နံပါတ် 6.0 ဖြစ်ကောင်းဖြစ်နိုင်သည်) တွင် ထည့်သွင်းရန်အတွက် RV (Runtime Verification) ယန္တရား၏ အကောင်အထည်ဖော်မှုနှင့်အတူ ဖာထေးမှုအစုတစ်ခုကို အဆိုပြုထားပြီး၊ ၎င်းအား အာမခံချက်ပေးသော အလွန်ယုံကြည်စိတ်ချရသော စနစ်များတွင် မှန်ကန်သောလုပ်ဆောင်ချက်ကို စစ်ဆေးရန်အတွက် ကိရိယာများကို ပံ့ပိုးပေးသည့် RV (Runtime Verification) ပျက်ကွက်မှုများမရှိခြင်း။ စနစ်၏မျှော်မှန်းထားသည့်အပြုအမူကိုသတ်မှတ်ပေးသည့် automaton ၏ကြိုတင်သတ်မှတ်ထားသောရည်ညွှန်းသတ်မှတ်စံနမူနာတစ်ခုနှင့် ပတ်သက်၍ ကိုင်တွယ်လုပ်ဆောင်သည့်အချက်များကိုခြေရာခံအချက်များဆီသို့ ကိုင်တွယ်သူများကို ပူးတွဲခြင်းဖြင့် အတည်ပြုခြင်းကို runtime တွင်လုပ်ဆောင်သည်။

ခြေရာခံအချက်များမှ အချက်အလက်များသည် မော်ဒယ်ကို ပြည်နယ်တစ်ခုမှ အခြားပြည်နယ်တစ်ခုသို့ ရွေ့လျားစေပြီး၊ ပြည်နယ်အသစ်သည် မော်ဒယ်၏ ကန့်သတ်ချက်များနှင့် မကိုက်ညီပါက၊ သတိပေးချက်တစ်ခု ထုတ်ပေးမည် သို့မဟုတ် kernel အား "ထိတ်လန့်ခြင်း" အခြေအနေတွင် ထားရှိသည် (ယုံကြည်စိတ်ချရမှုမြင့်မားသော စနစ်များကို ရှာဖွေနိုင်မည်ဟု မျှော်လင့်ပါသည်။ ထိုကဲ့သို့သော အခြေအနေများကို တုံ့ပြန်ပါ။) ပြည်နယ်တစ်ခုမှ တစ်ခုသို့ ကူးပြောင်းမှုများကို သတ်မှတ်သည့် automaton မော်ဒယ်ကို "dot" ဖော်မတ် (graphviz) သို့ တင်ပို့ပြီးနောက် ၎င်းကို dot2c utility ကို အသုံးပြု၍ C ကိုယ်စားပြုမှုအဖြစ်သို့ ပြန်ဆိုကာ၊ ၎င်းကို kernel module ပုံစံဖြင့် တင်ဆောင်သည့် ပုံစံ၊ ကြိုတင်သတ်မှတ်ထားသော မော်ဒယ်မှ လုပ်ဆောင်မှု တိုးတက်မှု၏ သွေဖီမှုများကို ခြေရာခံသည်။

Linux အတွက်၊ kernel ၏ မှန်ကန်သောလုပ်ဆောင်ချက်ကို အတည်ပြုရန် ယန္တရားတစ်ခု အဆိုပြုထားသည်။

Run-time model checking သည် mission-critical systems တွင် မှန်ကန်သော execution ကို အတည်ပြုရန် ပေါ့ပါးပြီး လွယ်ကူသော အကောင်အထည်ဖော်သည့်နည်းလမ်းအဖြစ် ရပ်တည်ထားပြီး၊ မော်ဒယ်စစ်ဆေးခြင်းနှင့် တရားဝင်သတ်မှတ်ပေးထားသည့် သတ်မှတ်ချက်များနှင့် ကိုက်ညီမှုရှိသော သင်္ချာအထောက်အထားများကဲ့သို့သော classical ယုံကြည်စိတ်ချရမှု အတည်ပြုခြင်းနည်းလမ်းများကို ဖြည့်စွက်ပေးပါသည်။ ဘာသာစကား။ RV ၏ အားသာချက်များထဲတွင် စနစ်တစ်ခုလုံးကို မော်ဒယ်လ်ဘာသာစကားဖြင့် သီးခြားအကောင်အထည်ဖော်ခြင်းမရှိဘဲ တင်းကျပ်သောအတည်ပြုချက်ကို ပေးစွမ်းနိုင်သည့်အပြင်၊ ဥပမာအားဖြင့်၊ မမြင်နိုင်သောဖြစ်ရပ်များအတွက် လိုက်လျောညီထွေရှိသော တုံ့ပြန်မှု၊ ဥပမာ၊ အရေးကြီးသောစနစ်များတွင် ချို့ယွင်းမှုတစ်ခု ထပ်မံပြန့်ပွားမှုကို ပိတ်ဆို့ရန်ဖြစ်သည်။

source: opennet.ru

မှတ်ချက် Add