लिनक्स के लिए, कर्नेल के सही संचालन को सत्यापित करने के लिए एक तंत्र प्रस्तावित किया गया है

लिनक्स कर्नेल 5.20 (शायद शाखा को 6.0 क्रमांकित किया जाएगा) में शामिल करने के लिए, आरवी (रनटाइम सत्यापन) तंत्र के कार्यान्वयन के साथ पैच का एक सेट प्रस्तावित है, जो अत्यधिक विश्वसनीय सिस्टम पर सही संचालन की जांच के लिए उपकरण प्रदान करता है जो गारंटी देता है असफलताओं का अभाव. रनटाइम पर हैंडलर्स को ट्रेस पॉइंट्स से जोड़कर सत्यापन किया जाता है जो ऑटोमेटन के पूर्व निर्धारित संदर्भ नियतात्मक मॉडल के खिलाफ निष्पादन की वास्तविक प्रगति की जांच करता है जो सिस्टम के अपेक्षित व्यवहार को परिभाषित करता है।

ट्रेस बिंदुओं से जानकारी मॉडल को एक राज्य से दूसरे राज्य में ले जाती है, और यदि नया राज्य मॉडल के मापदंडों से मेल नहीं खाता है, तो एक चेतावनी उत्पन्न होती है या कर्नेल को "घबराहट" स्थिति में रखा जाता है (उच्च विश्वसनीयता सिस्टम का पता लगाने की उम्मीद की जाती है) और ऐसी स्थितियों पर प्रतिक्रिया दें)। ऑटोमेटन मॉडल, जो एक राज्य से दूसरे राज्य में संक्रमण को परिभाषित करता है, को "डॉट" प्रारूप (ग्राफविज़) में निर्यात किया जाता है, जिसके बाद इसे dot2c उपयोगिता का उपयोग करके सी प्रतिनिधित्व में अनुवादित किया जाता है, जिसे कर्नेल मॉड्यूल के रूप में लोड किया जाता है पूर्वनिर्धारित मॉडल से निष्पादन प्रगति के विचलन को ट्रैक करता है।

रन-टाइम मॉडल चेकिंग को मिशन-क्रिटिकल सिस्टम पर सही निष्पादन की पुष्टि करने के लिए एक हल्के-वजन और आसानी से लागू होने वाली विधि के रूप में तैनात किया गया है, जो शास्त्रीय विश्वसनीयता सत्यापन विधियों जैसे कि मॉडल चेकिंग और औपचारिक में दिए गए विनिर्देशों के साथ कोड अनुपालन के गणितीय प्रमाणों को पूरक करता है। भाषा। आरवी के फायदों में से एक मॉडलिंग भाषा में पूरे सिस्टम के अलग कार्यान्वयन के बिना सख्त सत्यापन प्रदान करने की क्षमता है, साथ ही अप्रत्याशित घटनाओं के लिए लचीली प्रतिक्रिया भी है, उदाहरण के लिए, महत्वपूर्ण प्रणालियों में विफलता के आगे प्रसार को रोकना।

स्रोत: opennet.ru