औपचारिक सत्यापन
हार्डवेयर और सॉफ्टवेयर प्रणाली के संदर्भ में, औपचारिक सत्यापन गणित के औपचारिक विधियों का उपयोग करके एक निश्चित औपचारिक विनिर्देश या सामग्री के संबंध में एक प्रणाली के अंतर्निहित कलन विधि के गणितये प्रमाण की विशुद्धता को स्वीकार करने या अस्वीकार करने का कार्य है।[1]
यह औपचारिक सत्यापन प्रणाली की विशुद्धता को प्रमाणित करने में सहायक हो सकता है जैसे: क्रिप्टोग्राफिक प्रोटोकॉल, संयोजन तर्क, आंतरिक मेमोरी के साथ डिजिटल सर्किट और स्रोत कोड के रूप में व्यक्त सॉफ़्टवेयर।
इन प्रणालियों का सत्यापन प्रणाली के एक संक्षिप्त गणितीय प्रतिरूप पर एक औपचारिक प्रमाण प्रदान करके किया जाता है, गणितीय प्रतिरूप और प्रणाली की प्रकृति के मध्य पत्राचार को इसके अतिरिक्त निर्माण द्वारा जाना जाता है। गणितीय वस्तुओं के उदाहरण अधिकांशतः प्रतिरूप प्रणाली के लिए उपयोग किए जाते हैं: परिमित-स्थिति मशीनें, लेबल संक्रमण प्रणाली, पेट्री नेट, सदिश जोड़ प्रणाली, समयबद्ध ऑटोमेटन, हाइब्रिड ऑटोमेटा, प्रक्रिया बीजगणित, प्रोग्रामिंग भाषाओं के औपचारिक शब्दार्थ जैसे परिचालन शब्दार्थ, अर्थ शब्दार्थ, स्वयंसिद्ध शब्दार्थ और होरे तर्क ।[2]
दृष्टिकोण
यह एक दृष्टिकोण और गठन प्रतिरूप की मूल्यांकन है, जिसमें गणितीय प्रतिरूप का एक व्यवस्थित रूप से संपूर्ण अन्वेषण सम्मिलित है (यह परिमित प्रतिरूप सिद्धांत के लिए संभव है, लेकिन कुछ अनंत प्रतिरूप के लिए भी है जहाँ स्थितियों के अनंत अवयवों को अमूर्तता का उपयोग करके या लाभ उठाकर प्रभावी विधियों से प्रदर्शित किया जा सकता है।) सामान्यतः, इसमें एक ही संचालन में स्थितियों के पूरे समूह पर विचार करने और कंप्यूटिंग समय को कम करने के लिए सुव्यवस्थित और क्षेत्र-विशिष्ट अमूर्त तकनीकों का उपयोग करके प्रतिरूप में सभी स्थितियों और संक्रमणों की खोज करना सम्मिलित है। कार्यान्वयन तकनीकों में स्थिति अंतरिक्ष गणना, प्रतीकात्मक स्थिति अंतरिक्ष गणना, सार व्याख्या, प्रतीकात्मक अनुकरण, अमूर्त शोधन सम्मिलित हैं।[citation needed] प्रमाणित किए जाने वाले गुणों को अधिकांशतः लौकिक तर्क में वर्णित किया जाता है, जैसे रैखिक लौकिक तर्क (एलटीएल), संपत्ति विशिष्टता भाषा (पीएसएल), प्रणाली वेरिलॉग एसेर्शन (एसवीए),[3] या कम्प्यूटेशनल वृक्ष तर्क (CTL)। प्रतिरूप मूल्यांकन का बड़ा लाभ यह है कि यह अधिकांशतः पूरी तरह से स्वचालित होती है; इसकी प्राथमिक हानि यह है कि यह सामान्य रूप से बड़ी प्रणालियों के पैमाने पर नहीं होता है; प्रतीकात्मक प्रतिरूप सामान्य स्थिति के कुछ सौ बिट्स तक सीमित होते हैं, जबकि स्पष्ट स्थिति गणना के लिए अपेक्षाकृत छोटे होने के लिए इस प्रकार की स्थिति के स्थान की खोज की आवश्यकता होती है।
एक अन्य दृष्टिकोण निगनात्मक सत्यापन है। इसमें प्रणाली और इसकी विशिष्टताओं (और संभवतः अन्य टिप्पणियां) से गणितीय प्रमाणों के दायित्वों का एक संग्रह उत्पन्न होता है, जिसकी प्रमाणिकता प्रणाली के विनिर्देशों के अनुरूप होती है, और इन दायित्वों का निर्वहन या तो प्रमाण सहायकों (आकर्षक प्रमेय सिद्ध) का उपयोग करते हुए होता है ( जैसे कि होल प्रमेय सिद्ध, एसीएल 2, इसाबेल (प्रमेय सिद्ध), कोक (Coq) या प्रोटोटाइप सत्यापन प्रणाली ), या स्वचालित प्रमेय सिद्ध, विशेष रूप से संतुष्टि मोडुलो सिद्धांत (SMT) समाधानकर्ता सहित का उपयोग करते हुए होता है। इस दृष्टिकोण की हानि यह है कि इसके लिए उपयोगकर्ता को विस्तार से समझने की आवश्यकता हो सकती है कि प्रणाली सही विधि से क्यों काम करता है, और इस जानकारी को सत्यापन प्रणाली तक पहुंचाने के लिए, या तो सिद्ध किए जाने वाले प्रमेयों के अनुक्रम के रूप में या प्रणाली घटकों (जैसे कार्य या प्रक्रियाएं) और संभवतः उप-घटक (जैसे लूप या डेटा संरचना) के विनिर्देशों (अपरिवर्तनीय, पूर्व शर्त, पोस्टकंडिशन) के रूप में।
सॉफ्टवेयर
सॉफ्टवेयर प्रोग्राम के औपचारिक सत्यापन में यह प्रमाणित करना सम्मिलित है कि एक प्रोग्राम अपने व्यवहार के औपचारिक विनिर्देश को पूरा करता है। औपचारिक सत्यापन के उपक्षेत्रों में निगमनात्मक सत्यापन (ऊपर देखें), सार व्याख्या, स्वचालित प्रमेय सिद्ध करना, टाइप प्रणालियाँ, और प्रभाव रहित औपचारिक विधियाँ सम्मिलित हैं। एक आशाजनक प्रकार-आधारित सत्यापन दृष्टिकोण निर्भर रूप से टाइप की गई प्रोग्रामिंग है, जिसमें कार्यों के प्रकारों में उन कार्यों के विनिर्देश (कम से कम भाग) सम्मिलित हैं, और कोड का मूल्यांकन करना उन विशिष्टताओं के विरुद्ध इसकी विशुद्धता स्थापित करता है। विशेष स्थितियों के रूप में पूरी तरह से विशेष रुप से टाइप की गई भाषाएं निगनात्मक सत्यापन का समर्थन करती हैं।
यह एक अन्य पूरक दृष्टिकोण प्रोग्राम व्युत्पत्ति है, जिसमें विशुद्धता-संरक्षण चरणों की एक श्रृंखला द्वारा कार्यात्मक प्रोग्रामिंग विनिर्देशों से कुशल कोड का उत्पादन किया जाता है। इस दृष्टिकोण का एक उदाहरण बर्ड-मीर्टेंस औपचारिकता है, और इस दृष्टिकोण को निर्माण द्वारा सही के रूप में देखा जा सकता है।
ये तकनीकें ध्वनि हो सकती हैं, जिसका अर्थ है कि सत्यापित गुणों को शब्दार्थ से तार्किक रूप से घटाया जा सकता है, या असंदिग्ध, जिसका अर्थ है कि ऐसी कोई प्रमाणिकता नहीं है। एक ध्वनि तकनीक तभी परिणाम देती है जब वह संभावनाओं के पूरे स्थान को छुपा लेती है। एक गलत तकनीक का एक उदाहरण वह है जो संभावनाओं के केवल एक उपसमुच्चय को सम्मिलित करता है, उदाहरण के लिए केवल एक निश्चित संख्या तक पूर्णांक, और एक "पर्याप्त-पर्याप्त" परिणाम देता है। तकनीकें निर्णायक (तर्क) भी हो सकती हैं, जिसका अर्थ है कि उनके एल्गोरिथम कार्यान्वयन को एक उत्तर के साथ समाप्त करने की प्रमाणिकता दी जाती है, या अनिर्णीत, जिसका अर्थ है कि वे कभी भी समाप्त नहीं हो सकते हैं। संभावनाओं के कार्यक्षेत्र को सीमित करके, कोई भी निर्णायक ध्वनि तकनीक उपलब्ध नहीं होने पर अस्वास्थ्यकर तकनीकों का निर्माण किया जा सकता है।
सत्यापन और वैधता
सत्यापन और वैधता उद्देश्य के लिए किसी उत्पाद की उपयुक्तता के परीक्षण का एक पहलू है और मान्यता पूरक पहलू है। अधिकांशतः एक समग्र मूल्यांकन प्रक्रिया सत्यापन और वैधता को वी और वी के रूप में संदर्भित करता है।
- मान्यता: "क्या हम सही काम करने का प्रयास कर रहे थे?", यानी, उत्पाद उपयोगकर्ता की वास्तविक आवश्कताओं के लिए निर्दिष्ट है?
- सत्यापन: "क्या हमने वह बनाया है जो हम बनाने का प्रयास कर रहे थे?", यानी, उत्पाद विनिर्देशों के अनुरूप है?
सत्यापन प्रक्रिया में स्थिर/संरचनात्मक और गतिशील/व्यवहारिक पहलू सम्मिलित हैं। उदाहरण के लिए, एक सॉफ्टवेयर उत्पाद के लिए कोई स्रोत कोड (स्थैतिक) का निरीक्षण कर सकता है और विशिष्ट परीक्षण स्थितियों (गतिशील) के विरूद्ध चल सकता है। सत्यापन सामान्यतः केवल गतिशील रूप से किया जा सकता है, अर्थात, उत्पाद को विशिष्ट और असामान्य उपयोगों के माध्यम से परीक्षण किया जाता है ("क्या यह संतोषजनक रूप से सभी उपयोग स्थितियों को पूरा करता है?")।
स्वचालित कार्यक्रम का सुधार
प्रोग्राम का सुधार ओरेकल (कम्प्यूटेबिलिटी) के संबंध में किया जाती है, जिसमें प्रोग्राम की वांछित कार्यक्षमता सम्मिलित होती है जिसका उपयोग उत्पन्न किए गए फिक्स के सत्यापन के लिए किया जाता है। इसका एक सरल उदाहरण एक टेस्ट-सूट है- इनपुट/आउटपुट जोड़े प्रोग्राम की कार्यक्षमता निर्दिष्ट करते हैं।विभिन्न प्रकार की तकनीकों को नियोजित किया जाता है, विशेष रूप से संतुष्टि मॉडुलो प्रमेय (एसएमटी), समाधानकर्ता,[4] और आनुवंशिक प्रोग्रामिंग,[5] विकासवादी कंप्यूटिंग का उपयोग करते हुए फिक्स के लिए संभावित उम्मीदवारों को उत्पन्न करने और उनका मूल्यांकन करने के लिए पूर्व पद्धति नियतात्मक है, जबकि बाद वाली यादृच्छिक है।
यह कार्यक्रम का सुधार औपचारिक सत्यापन और कार्यक्रम संश्लेषण की तकनीकों को जोड़ती है। औपचारिक सत्यापन में दोष-स्थानीयकरण तकनीकों का उपयोग प्रोग्राम बिंदुओं की गणना करने के लिए किया जाता है जो संभावित बग-स्थान हो सकते हैं, जिन्हें संश्लेषण मॉड्यूल द्वारा लक्षित किया जा सकता है। खोज स्थान को कम करने के लिए सुधार प्रणालियां अधिकांशतः बग के एक छोटे पूर्व-निर्धारित वर्ग पर ध्यान केंद्रित करती हैं। उपस्थित तकनीकों की कम्प्यूटेशनल लागत के कारण औद्योगिक उपयोग सीमित है।
उद्योगों में उपयोग
प्रारूपों की जटिलता में वृद्धि हार्डवेयर उद्योग में औपचारिक सत्यापन तकनीकों के महत्व को बढ़ाती है।[6][7] वर्तमान में, अधिकांश या सभी प्रमुख हार्डवेयर कंपनियों द्वारा औपचारिक सत्यापन का उपयोग किया जाता है,[8] लेकिन सॉफ्टवेयर उद्योग में इसका उपयोग अभी भी कम हो रहा है।[citation needed] इसे हार्डवेयर उद्योग में अधिक आवश्यकता के लिए उत्तरदायी ठहराया जा सकता है, जहां त्रुटियों का व्यावसायिक महत्व अधिक होता है।[citation needed] घटकों के बीच संभावित सूक्ष्म अंतःक्रियाओं के कारण, अनुकरण द्वारा संभावनाओं के यथार्थवादी समुच्चय का प्रयोग करना कठिन होता जा रहा है। हार्डवेयर प्रारूप के महत्वपूर्ण पहलू स्वचालित सिद्ध विधियों के लिए उत्तरदायी हैं, औपचारिक सत्यापन को शुरू करना सहज और अधिक उत्पादक बनाते हैं।[9]
2011 तक, कई ऑपरेटिंग प्रणाली औपचारिक रूप से सत्यापित किए गए हैं: निक्टा का सुरक्षित L4 माइक्रोकर्नेल, OK लैब्स द्वारा seL4 के रूप में व्यावसायिक रूप से बेचा गया;[10] पूर्वी चीन सामान्य विश्वविद्यालय द्वारा ओएसेक/वीडीएक्स आधारित रीयल-टाइम ऑपरेटिंग प्रणाली ओरिएंटैस ;[citation needed] ग्रीन हिल्स सॉफ्टवेयर की सच्चाई (ऑपरेटिंग प्रणाली );[citation needed] और SYSGO का पाइकोस।[11][12] 2016 में, येल में झोंग शाओ के नेतृत्व में एक टीम ने CertiKOS नामक एक औपचारिक रूप से सत्यापित ऑपरेटिंग प्रणाली कर्नेल विकसित किया।[13][14] 2017 तक, नेटवर्क के गणितीय प्रतिरूप के माध्यम से बड़े कंप्यूटर नेटवर्क के प्रारूप के लिए औपचारिक सत्यापन लागू किया गया है,[15] और एक नई नेटवर्क प्रौद्योगिकी श्रेणी, आशय-आधारित नेटवर्किंग के आदान प्रदान करने के रूप में।[16] औपचारिक सत्यापन समाधान प्रदान करने वाले नेटवर्क सॉफ़्टवेयर विक्रेताओं में सिस्को सम्मिलित है[17] फॉरवर्ड नेटवर्क[18][19] और वेरिफ्लो प्रणाली सम्मिलित है।[20]
स्पार्क (प्रोग्रामिंग भाषा) एक टूलसेट प्रदान करता है जो औपचारिक सत्यापन के साथ सॉफ्टवेयर विकास को सक्षम बनाता है और अनुप्रयोग कई उच्च-अखंडता प्रणालियों में उपयोग किया जाता है।[citation needed]
कॉम्पर्ट सी संकलक एक औपचारिक रूप से सत्यापित सी संकलक है जो अधिकांश आईएसओ सी को लागू करता है।[citation needed]
यह भी देखें
- स्वचालित प्रमेय प्रमाणित करना
- प्रतिरूप मूल्यांकन
- प्रतिरूप मूल्यांकन उपकरणों की सूची
- औपचारिक तुल्यता मूल्यांकन
- सबूत चेकर
- संपत्ति विशिष्टता भाषा
- सैद्धांतिक कंप्यूटर विज्ञान में महत्वपूर्ण प्रकाशनों की सूची #औपचारिक सत्यापन
- स्टेटिक कोड विश्लेषण
- परिमित-स्थिति सत्यापन में अस्थायी तर्क
- पोस्ट-सिलिकॉन सत्यापन
- बुद्धिमान सत्यापन
- रनटाइम सत्यापन
संदर्भ
- ↑ Sanghavi, Alok (May 21, 2010). "औपचारिक सत्यापन क्या है?". EE Times Asia.
- ↑ Introduction to Formal Verification, Berkeley University of California, Retrieved November 6, 2013
- ↑ Cohen, Ben; Venkataramanan, Srinivasan; Kumari, Ajeetha; Piper, Lisa (2015). SystemVerilog अभिकथन हैंडबुक (4th ed.). CreateSpace Independent Publishing Platform. ISBN 978-1518681448.
- ↑ Favio DeMarco; Jifeng Xuan; Daniel Le Berre; Martin Monperrus (2014). बग्गी की स्वचालित मरम्मत यदि स्थितियाँ और एसएमटी के साथ पूर्व शर्त नहीं हैं. pp. 30–39. arXiv:1404.3186. doi:10.1145/2593735.2593740. ISBN 9781450328470. S2CID 506586.
{{cite book}}:|journal=ignored (help) - ↑ Le Goues, Claire; Nguyen, ThanhVu; Forrest, Stephanie; Weimer, Westley (January 2012). "GenProg: स्वचालित सॉफ़्टवेयर मरम्मत के लिए एक सामान्य विधि". IEEE Transactions on Software Engineering. 38 (1): 54–72. doi:10.1109/TSE.2011.104. S2CID 4111307.
- ↑ Harrison, J. (2003). "Formal verification at Intel". कम्प्यूटर साइंस में लॉजिक का 18वां वार्षिक IEEE संगोष्ठी, 2003। कार्यवाही. pp. 45–54. doi:10.1109/LICS.2003.1210044. ISBN 978-0-7695-1884-8. S2CID 44585546.
- ↑ Formal verification of a real-time hardware design. Portal.acm.org (June 27, 1983). Retrieved on April 30, 2011.
- ↑ "औपचारिक सत्यापन: एरिक सेलिगमैन, टॉम शुबर्ट, और एमवी अच्युता किरणकुमार द्वारा आधुनिक वीएलएसआई डिजाइन के लिए एक आवश्यक उपकरण". 2015.
- ↑ "उद्योग में औपचारिक सत्यापन" (PDF). Retrieved September 20, 2012.
- ↑ "SEL4/ARMv6 API का सार औपचारिक विशिष्टता" (PDF). Archived from the original (PDF) on May 21, 2015. Retrieved May 19, 2015.
- ↑ Christoph Baumann, Bernhard Beckert, Holger Blasum, and Thorsten Bormer Ingredients of Operating System Correctness? Lessons Learned in the Formal Verification of PikeOS
- ↑ "Getting it Right" by Jack Ganssle
- ↑ Harris, Robin. "हैक नहीं किया जा सकने वाला OS? CertiKOS सुरक्षित सिस्टम कर्नेल के निर्माण को सक्षम करता है". ZDNet. Retrieved June 10, 2019.
- ↑ "CertiKOS: येल ने दुनिया का पहला हैकर प्रतिरोधी ऑपरेटिंग सिस्टम विकसित किया है". International Business Times UK. November 15, 2016. Retrieved June 10, 2019.
- ↑ Scroxton, Alex. "सिस्को के लिए, आशय-आधारित नेटवर्किंग भविष्य की तकनीकी मांगों की शुरुआत करती है". Computer Weekly. Retrieved February 12, 2018.
- ↑ Lerner, Andrew. "आशय आधारित नेटवर्किंग". Gartner. Retrieved February 12, 2018.
- ↑ Kerravala, Zeus. "सिस्को इंटेंट आधारित नेटवर्क को डेटा सेंटर में लाता है". NetworkWorld. Retrieved February 12, 2018.
- ↑ "फॉरवर्ड नेटवर्क: त्वरित और डी-जोखिम नेटवर्क संचालन". Insights Success. Retrieved February 12, 2018.
- ↑ "इंटेंट = आधारित नेटवर्किंग में ग्राउंडेड होना" (PDF). NetworkWorld. Retrieved February 12, 2018.
- ↑ "वेरिफ्लो सिस्टम्स". Bloomberg. Retrieved February 12, 2018.
