লিনাক্সের জন্য, কার্নেলের সঠিক অপারেশন যাচাই করার জন্য একটি প্রক্রিয়া প্রস্তাব করা হয়েছে

লিনাক্স কার্নেল 5.20 (সম্ভবত শাখাটির সংখ্যা 6.0) এ অন্তর্ভুক্ত করার জন্য, RV (রানটাইম যাচাইকরণ) পদ্ধতি বাস্তবায়নের সাথে প্যাচের একটি সেট প্রস্তাব করা হয়েছে, যা অত্যন্ত নির্ভরযোগ্য সিস্টেমে সঠিক অপারেশন চেক করার জন্য সরঞ্জাম সরবরাহ করে যা গ্যারান্টি দেয় ব্যর্থতার অনুপস্থিতি। সিস্টেমের প্রত্যাশিত আচরণকে সংজ্ঞায়িত করে অটোমেটনের পূর্বনির্ধারিত রেফারেন্স ডিটারমিনিস্টিক মডেলের বিপরীতে কার্য সম্পাদনের প্রকৃত অগ্রগতি পরীক্ষা করে এমন পয়েন্টে হ্যান্ডলারদের সংযুক্ত করে রানটাইমে যাচাইকরণ করা হয়।

ট্রেস পয়েন্ট থেকে তথ্য মডেলটিকে এক স্টেট থেকে অন্য স্টেটে নিয়ে যায়, এবং যদি নতুন স্টেট মডেলের প্যারামিটারের সাথে মেলে না, তাহলে একটি সতর্কতা তৈরি করা হয় বা কার্নেলটিকে একটি "আতঙ্ক" অবস্থায় রাখা হয় (উচ্চ নির্ভরযোগ্যতা সিস্টেমগুলি সনাক্ত করতে পারে বলে আশা করা হয়) এবং এই ধরনের পরিস্থিতিতে সাড়া)। অটোমেটন মডেল, যা এক রাজ্য থেকে অন্য অবস্থার রূপান্তরকে সংজ্ঞায়িত করে, "ডট" ফর্ম্যাটে (গ্রাফভিজ) রপ্তানি করা হয়, তারপরে এটি ডট2সি ইউটিলিটি ব্যবহার করে একটি সি উপস্থাপনায় অনুবাদ করা হয়, যা একটি কার্নেল মডিউল আকারে লোড করা হয়। পূর্বনির্ধারিত মডেল থেকে সঞ্চালনের অগ্রগতির বিচ্যুতি ট্র্যাক করে।

রান-টাইম মডেল চেকিংকে মিশন-ক্রিটিকাল সিস্টেমে সঠিক সম্পাদন যাচাই করার জন্য একটি হালকা-ওজন এবং সহজে-বাস্তবায়ন পদ্ধতি হিসাবে অবস্থান করা হয়েছে, ক্লাসিক্যাল নির্ভরযোগ্যতা যাচাইকরণ পদ্ধতি যেমন মডেল চেকিং এবং আনুষ্ঠানিকভাবে প্রদত্ত স্পেসিফিকেশনের সাথে কোড সম্মতির গাণিতিক প্রমাণের পরিপূরক। ভাষা. RV-এর সুবিধার মধ্যে একটি মডেলিং ভাষায় সম্পূর্ণ সিস্টেমের একটি পৃথক প্রয়োগ ছাড়াই কঠোর যাচাইকরণ প্রদান করার ক্ষমতা, সেইসাথে অপ্রত্যাশিত ঘটনাগুলির নমনীয় প্রতিক্রিয়া, উদাহরণস্বরূপ, সমালোচনামূলক সিস্টেমে ব্যর্থতার আরও প্রচারকে ব্লক করা।

উত্স: opennet.ru