लिनक्सको लागि, कर्नेलको सही सञ्चालन प्रमाणित गर्न एउटा संयन्त्र प्रस्तावित गरिएको छ

लिनक्स कर्नेल 5.20 मा समावेश गर्नका लागि (सायद शाखा नम्बर 6.0 हुनेछ), RV (रनटाइम प्रमाणिकरण) संयन्त्रको कार्यान्वयनको साथ प्याचहरूको सेट प्रस्ताव गरिएको छ, जसले अत्यधिक भरपर्दो प्रणालीहरूमा सही सञ्चालन जाँच गर्न उपकरणहरू प्रदान गर्दछ जसले ग्यारेन्टी गर्दछ। असफलता को अनुपस्थिति। प्रमाणिकरण रनटाइममा ह्यान्डलरहरूलाई ट्रेस पोइन्टहरूमा संलग्न गरेर प्रदर्शन गरिन्छ जसले प्रणालीको अपेक्षित व्यवहार परिभाषित गर्ने अटोमेटनको पूर्वनिर्धारित सन्दर्भ निर्धारणवादी मोडेल विरुद्ध कार्यान्वयनको वास्तविक प्रगति जाँच गर्दछ।

ट्रेस पोइन्टहरूबाट जानकारीले मोडेललाई एक राज्यबाट अर्कोमा सार्छ, र यदि नयाँ अवस्था मोडेलको प्यारामिटरहरूसँग मेल खाँदैन भने, चेतावनी उत्पन्न हुन्छ वा कर्नेललाई "आतंक" स्थितिमा राखिएको हुन्छ (उच्च विश्वसनीयता प्रणालीहरूले पत्ता लगाउने अपेक्षा गरिन्छ। र त्यस्ता परिस्थितिहरूमा प्रतिक्रिया दिनुहोस्)। अटोमेटन मोडेल, जसले एक राज्यबाट अर्को राज्यमा ट्रान्जिसनहरू परिभाषित गर्दछ, "डट" ढाँचा (ग्राफभिज) मा निर्यात गरिन्छ, त्यसपछि यसलाई C प्रतिनिधित्वमा dot2c उपयोगिता प्रयोग गरी अनुवाद गरिन्छ, जुन कर्नेल मोड्युलको रूपमा लोड हुन्छ। पूर्वनिर्धारित मोडेलबाट कार्यान्वयन प्रगतिको विचलन ट्र्याक गर्दछ।

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

स्रोत: opennet.ru