औपचारिक सत्यापन

Not to be confused with Verificationism. For the Wikipedia policy, see Wikipedia:Verifiability.

हार्डवेयर और सॉफ्टवेयर प्रणाली के संदर्भ में, औपचारिक सत्यापन गणित के औपचारिक विधियों का उपयोग करके एक निश्चित औपचारिक विनिर्देश या सामग्री के संबंध में एक प्रणाली के अंतर्निहित कलन विधि के गणितये प्रमाण की विशुद्धता को स्वीकार करने या अस्वीकार करने का कार्य है।

यह औपचारिक सत्यापन प्रणाली की विशुद्धता को प्रमाणित करने में सहायक हो सकता है जैसे: क्रिप्टोग्राफिक प्रोटोकॉल , संयोजन तर्क , आंतरिक मेमोरी के साथ डिजिटल सर्किट और स्रोत कोड के रूप में व्यक्त सॉफ़्टवेयर।

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

दृष्टिकोण

यह एक दृष्टिकोण और गठन प्रतिरूप की मूल्यांकन है, जिसमें गणितीय प्रतिरूप का एक व्यवस्थित रूप से संपूर्ण अन्वेषण सम्मिलित है (यह परिमित प्रतिरूप सिद्धांत के लिए संभव है, लेकिन कुछ अनंत प्रतिरूप के लिए भी है जहाँ स्थितियों के अनंत अवयवों को अमूर्तता का उपयोग करके या लाभ उठाकर प्रभावी विधियों से प्रदर्शित किया जा सकता है।) सामान्यतः, इसमें एक ही संचालन में स्थितियों के पूरे समूह पर विचार करने और कंप्यूटिंग समय को कम करने के लिए सुव्यवस्थित और क्षेत्र-विशिष्ट अमूर्त तकनीकों का उपयोग करके प्रतिरूप में सभी स्थितियों और संक्रमणों की खोज करना सम्मिलित है। कार्यान्वयन तकनीकों में स्थिति अंतरिक्ष गणना , प्रतीकात्मक स्थिति अंतरिक्ष गणना, सार व्याख्या , प्रतीकात्मक अनुकरण , अमूर्त शोधन सम्मिलित हैं। प्रमाणित किए जाने वाले गुणों को अधिकांशतः लौकिक तर्क में वर्णित किया जाता है, जैसे रैखिक लौकिक तर्क (एलटीएल), संपत्ति विशिष्टता भाषा (पीएसएल), प्रणाली वेरिलॉग एसेर्शन (एसवीए), या कम्प्यूटेशनल वृक्ष तर्क (CTL)। प्रतिरूप मूल्यांकन का बड़ा लाभ यह है कि यह अधिकांशतः पूरी तरह से स्वचालित होती है; इसकी प्राथमिक हानि यह है कि यह सामान्य रूप से बड़ी प्रणालियों के पैमाने पर नहीं होता है; प्रतीकात्मक प्रतिरूप सामान्य स्थिति के कुछ सौ बिट्स तक सीमित होते हैं, जबकि स्पष्ट स्थिति गणना के लिए अपेक्षाकृत छोटे होने के लिए इस प्रकार की स्थिति के स्थान की खोज की आवश्यकता होती है।

एक अन्य दृष्टिकोण निगनात्मक सत्यापन है। इसमें प्रणाली और इसकी विशिष्टताओं (और संभवतः अन्य टिप्पणियां) से गणितीय प्रमाणों के दायित्वों का एक संग्रह उत्पन्न होता है, जिसकी प्रमाणिकता प्रणाली के विनिर्देशों के अनुरूप होती है, और इन दायित्वों का निर्वहन या तो प्रमाण सहायकों (आकर्षक प्रमेय सिद्ध) का उपयोग करते हुए होता है ( जैसे कि होल प्रमेय सिद्ध, एसीएल 2 , इसाबेल (प्रमेय सिद्ध), कोक (Coq) या प्रोटोटाइप सत्यापन प्रणाली ), या स्वचालित प्रमेय सिद्ध, विशेष रूप से संतुष्टि मोडुलो सिद्धांत (SMT) समाधानकर्ता सहित का उपयोग करते हुए होता है। इस दृष्टिकोण की हानि यह है कि इसके लिए उपयोगकर्ता को विस्तार से समझने की आवश्यकता हो सकती है कि प्रणाली सही विधि से क्यों काम करता है, और इस जानकारी को सत्यापन प्रणाली तक पहुंचाने के लिए, या तो सिद्ध किए जाने वाले प्रमेयों के अनुक्रम के रूप में या प्रणाली घटकों (जैसे कार्य या प्रक्रियाएं) और संभवतः उप-घटक (जैसे लूप या डेटा संरचना) के विनिर्देशों (अपरिवर्तनीय, पूर्व शर्त, पोस्टकंडिशन) के रूप में।

सॉफ्टवेयर

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

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

ये तकनीकें सुदृढ़ता हो सकती हैं, जिसका अर्थ है कि सत्यापित गुणों को शब्दार्थ से तार्किक रूप से निकाला जा सकता है, या असंदिग्ध, जिसका अर्थ है कि ऐसी कोई गारंटी नहीं है। एक ध्वनि तकनीक तभी परिणाम देती है जब वह संभावनाओं के पूरे स्थान को कवर कर लेती है। एक गलत तकनीक का एक उदाहरण वह है जो संभावनाओं के केवल एक सबसेट को सम्मिलित करता है, उदाहरण के लिए केवल एक निश्चित संख्या तक पूर्णांक, और एक अच्छा-पर्याप्त परिणाम देता है। तकनीकें निर्णायकता (तर्क) भी हो सकती हैं, जिसका अर्थ है कि उनके एल्गोरिथम कार्यान्वयन एक उत्तर के साथ समाप्ति विश्लेषण हैं, या अनिर्णीत हैं, जिसका अर्थ है कि वे कभी भी समाप्त नहीं हो सकते हैं। संभावनाओं के दायरे को सीमित करके, कोई भी निर्णायक ध्वनि तकनीक उपलब्ध नहीं होने पर अस्वास्थ्यकर तकनीकों का निर्माण किया जा सकता है।

सत्यापन और सत्यापन

Main article: Verification and validation

सत्यापन और सत्यापन उद्देश्य के लिए किसी उत्पाद की फिटनेस के परीक्षण का एक पहलू है। मान्यता पूरक पहलू है। अधिकांशतः एक समग्र मूल्यांकन प्रक्रिया को सत्यापन और सत्यापन | वी एंड वी के रूप में संदर्भित करता है।

• मान्यता: क्या हम सही चीज़ बनाने की कोशिश कर रहे हैं? , यानी, उत्पाद उपयोगकर्ता की वास्तविक जरूरतों के लिए निर्दिष्ट है?
• सत्यापन: क्या हमने वह बनाया है जो हम बनाने की कोशिश कर रहे थे? , यानी, उत्पाद विनिर्देशों के अनुरूप है?

सत्यापन प्रक्रिया में स्थिर/संरचनात्मक और गतिशील/व्यवहारिक पहलू सम्मिलित हैं। उदाहरण के लिए, एक सॉफ्टवेयर उत्पाद के लिए कोई स्रोत कोड (स्थैतिक) का निरीक्षण कर सकता है और विशिष्ट परीक्षण मामलों (गतिशील) के खिलाफ चल सकता है। सत्यापन सामान्यतः केवल गतिशील रूप से किया जा सकता है, अर्थात, उत्पाद को विशिष्ट और असामान्य उपयोगों के माध्यम से रखकर परीक्षण किया जाता है (क्या यह संतोषजनक रूप से सभी उपयोग मामलों को पूरा करता है?)।

स्वचालित कार्यक्रम की मरम्मत

Main article: Automatic bug fixing

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

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

उद्योग उपयोग

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

As of 2011, कई ऑपरेटिंग प्रणाली औपचारिक रूप से सत्यापित किए गए हैं: NICTA का सुरक्षित L4 माइक्रोकर्नेल परिवार # न्यू साउथ वेल्स विश्वविद्यालय और NICTA, OK लैब्स द्वारा seL4 के रूप में व्यावसायिक रूप से बेचा गया; पूर्वी चीन सामान्य विश्वविद्यालय द्वारा OSEK/VDX आधारित रीयल-टाइम ऑपरेटिंग प्रणाली ORIENTAIS; ग्रीन हिल्स सॉफ्टवेयर की वफ़ादारी (ऑपरेटिंग प्रणाली ); और SYSGO का PikeOS । 2016 में, येल में झोंग शाओ के नेतृत्व में एक टीम ने CertiKOS नामक एक औपचारिक रूप से सत्यापित ऑपरेटिंग प्रणाली कर्नेल विकसित किया। 2017 तक, नेटवर्क के गणितीय प्रतिरूप के माध्यम से बड़े कंप्यूटर नेटवर्क के डिजाइन के लिए औपचारिक सत्यापन लागू किया गया है, और एक नई नेटवर्क प्रौद्योगिकी श्रेणी, आशय-आधारित नेटवर्किंग के हिस्से के रूप में। औपचारिक सत्यापन समाधान प्रदान करने वाले नेटवर्क सॉफ़्टवेयर विक्रेताओं में सिस्को सम्मिलित है फॉरवर्ड नेटवर्क और वेरिफ्लो प्रणाली ्स। स्पार्क (प्रोग्रामिंग भाषा) एक टूलसेट प्रदान करता है जो औपचारिक सत्यापन के साथ सॉफ्टवेयर विकास को सक्षम बनाता है और स्पार्क (प्रोग्रामिंग भाषा)#औद्योगिक अनुप्रयोग|कई उच्च-अखंडता प्रणालियों में उपयोग किया जाता है। CompCert एक औपचारिक रूप से सत्यापित C संकलक है जो अधिकांश ISO C को लागू करता है।

यह भी देखें

• स्वचालित प्रमेय प्रमाणित करना
• प्रतिरूप मूल्यांकन
• प्रतिरूप मूल्यांकन उपकरणों की सूची
• औपचारिक तुल्यता मूल्यांकन
• सबूत चेकर
• संपत्ति विशिष्टता भाषा
• सैद्धांतिक कंप्यूटर विज्ञान में महत्वपूर्ण प्रकाशनों की सूची #औपचारिक सत्यापन
• स्टेटिक कोड विश्लेषण
• परिमित-स्थिति सत्यापन में अस्थायी तर्क
• पोस्ट-सिलिकॉन सत्यापन
• बुद्धिमान सत्यापन
• रनटाइम सत्यापन

इस पेज में लापता आंतरिक लिंक की सूची

• अंक शास्त्र
• औपचारिक तरीके
• गणित का प्रतिरूप
• सोर्स कोड
• परिमित अवस्था मशीन
• सांकेतिक शब्दार्थ
• समयबद्ध automaton
• संतुष्टि मॉड्यूल सिद्धांत
• स्वचालित प्रमेय प्रमाणित करना
• एचओएल प्रमेय समर्थक
• इसाबेल (सिद्धांत प्रमाणित करें)
• सबूत सहायक
• कार्यक्रम व्युत्पत्ति
• प्रकार प्रणाली
• आश्रित प्रकार
• मूल्यांकन और वैधता
• अखंडता (ऑपरेटिंग प्रणाली )
• स्थैतिक कोड विश्लेषण