लिनक्ससाठी, कर्नलच्या योग्य ऑपरेशनची पडताळणी करण्यासाठी एक यंत्रणा प्रस्तावित करण्यात आली आहे

लिनक्स कर्नल 5.20 (कदाचित शाखा क्रमांक 6.0) मध्ये समाविष्ट करण्यासाठी, RV (रनटाइम पडताळणी) यंत्रणेच्या अंमलबजावणीसह पॅचेसचा एक संच प्रस्तावित केला आहे, जो अत्यंत विश्वासार्ह प्रणालींवर योग्य ऑपरेशन तपासण्यासाठी साधने प्रदान करतो. अपयशांची अनुपस्थिती. रनटाइममध्ये हँडलरला ट्रेस पॉइंट्सशी संलग्न करून पडताळणी केली जाते जी सिस्टमच्या अपेक्षित वर्तनाची व्याख्या करणाऱ्या ऑटोमॅटनच्या पूर्वनिर्धारित संदर्भ निर्धारक मॉडेलच्या विरूद्ध अंमलबजावणीची वास्तविक प्रगती तपासतात.

ट्रेस बिंदूंवरील माहिती मॉडेलला एका स्थितीतून दुसऱ्या स्थितीत हलवते आणि नवीन स्थिती मॉडेलच्या पॅरामीटर्सशी जुळत नसल्यास, एक चेतावणी तयार केली जाते किंवा कर्नल "पॅनिक" स्थितीत ठेवली जाते (उच्च विश्वसनीयता प्रणाली शोधणे अपेक्षित आहे. आणि अशा परिस्थितींना प्रतिसाद द्या). ऑटोमॅटन ​​मॉडेल, जे एका राज्यातून दुसऱ्या स्थितीत संक्रमण परिभाषित करते, ते "डॉट" फॉरमॅट (ग्राफविझ) मध्ये निर्यात केले जाते, त्यानंतर ते dot2c युटिलिटी वापरून C प्रस्तुतीकरणात अनुवादित केले जाते, जे कर्नल मॉड्यूलच्या रूपात लोड केले जाते. पूर्वनिर्धारित मॉडेलमधून अंमलबजावणी प्रगतीचे विचलन ट्रॅक करते.

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

स्त्रोत: opennet.ru