औपचारिक सत्यापन: Difference between revisions
No edit summary |
No edit summary |
||
| Line 16: | Line 16: | ||
== दृष्टिकोण == | == दृष्टिकोण == | ||
एक दृष्टिकोण और गठन [[ मॉडल की जाँच | प्रतिरूप की जाँच]] है, जिसमें गणितीय प्रतिरूप का एक व्यवस्थित रूप से संपूर्ण अन्वेषण | यह एक दृष्टिकोण और गठन [[ मॉडल की जाँच | प्रतिरूप की जाँच]] है, जिसमें गणितीय प्रतिरूप का एक व्यवस्थित रूप से संपूर्ण अन्वेषण सम्मिलित है (यह [[ परिमित मॉडल सिद्धांत | परिमित प्रतिरूप सिद्धांत]] के लिए संभव है, लेकिन कुछ अनंत प्रतिरूप के लिए भी है जहाँ स्थितों के अनंत अवयवों को अमूर्तता का उपयोग करके या लाभ उठाकर प्रभावी विधियों से प्रदर्शित किया जा सकता है। आमतौर पर, इसमें एक ही ऑपरेशन में स्थितिों के पूरे समूह पर विचार करने और कंप्यूटिंग समय को कम करने के लिए स्मार्ट और डोमेन-विशिष्ट अमूर्त तकनीकों का उपयोग करके प्रतिरूप में सभी स्थितिों और संक्रमणों की खोज करना सम्मिलित है। कार्यान्वयन तकनीकों में [[ राज्य अंतरिक्ष गणना | स्थिति अंतरिक्ष गणना]] , प्रतीकात्मक स्थिति अंतरिक्ष गणना, [[ सार व्याख्या ]], [[ प्रतीकात्मक अनुकरण ]], अमूर्त शोधन सम्मिलित हैं।{{citation needed|date=December 2014}} सत्यापित किए जाने वाले गुणों को अधिकांशतः [[ लौकिक तर्क ]]्स में वर्णित किया जाता है, जैसे [[ रैखिक लौकिक तर्क ]] (एलटीएल), [[ संपत्ति विशिष्टता भाषा ]] (पीएसएल), [[ सिस्टम वेरिलॉग | प्रणाली वेरिलॉग]] एसेर्शन (एसवीए),<ref>{{Cite book|title = SystemVerilog अभिकथन हैंडबुक|edition = 4th |last1 = Cohen|first1 = Ben| first2=Srinivasan |last2 =Venkataramanan |first3=Ajeetha |last3 =Kumari |first4=Lisa |last4 =Piper | publisher = CreateSpace Independent Publishing Platform|year = 2015|isbn = 978-1518681448}}</ref> या [[ कम्प्यूटेशनल वृक्ष तर्क ]] (CTL)। प्रतिरूप जाँच का बड़ा फायदा यह है कि यह अधिकांशतः पूरी तरह से स्वचालित होती है; इसका प्राथमिक नुकसान यह है कि यह सामान्य रूप से बड़ी प्रणालियों के पैमाने पर नहीं होता है; प्रतीकात्मक प्रतिरूप आमतौर पर स्थिति के कुछ सौ बिट्स तक सीमित होते हैं, जबकि स्पष्ट स्थिति गणना के लिए अपेक्षाकृत छोटे होने के लिए स्थिति स्थान की खोज की आवश्यकता होती है। | ||
एक अन्य दृष्टिकोण कटौतीत्मक सत्यापन है। इसमें प्रणाली और इसकी विशिष्टताओं (और संभवतः अन्य एनोटेशन) से गणितीय प्रमाण दायित्वों का एक संग्रह उत्पन्न होता है, जिसकी सच्चाई प्रणाली के विनिर्देशों के अनुरूप होती है, और इन दायित्वों का निर्वहन या तो प्रूफ सहायकों (इंटरैक्टिव प्रमेय प्रोवर्स) का उपयोग करते हुए होता है ( जैसे कि HOL प्रमेय सिद्ध, [[ ACL2 ]], इसाबेल (प्रमेय सिद्ध), [[ Coq ]] या [[ प्रोटोटाइप सत्यापन प्रणाली ]]), या स्वचालित प्रमेय सिद्ध, विशेष रूप से संतुष्टि मोडुलो सिद्धांत (SMT) सॉल्वर सहित। इस दृष्टिकोण का नुकसान यह है कि इसके लिए उपयोगकर्ता को विस्तार से समझने की आवश्यकता हो सकती है कि प्रणाली सही तरीके से क्यों काम करता है, और इस जानकारी को सत्यापन प्रणाली तक पहुंचाने के लिए, या तो प्रमेयों के अनुक्रम के रूप में या विनिर्देशों के रूप में ( प्रणाली घटकों (जैसे कार्य या प्रक्रियाएं) और शायद उप-घटक (जैसे लूप या डेटा संरचनाएं) के अपरिवर्तनीय, पूर्व शर्त, पोस्टकंडिशन)। | एक अन्य दृष्टिकोण कटौतीत्मक सत्यापन है। इसमें प्रणाली और इसकी विशिष्टताओं (और संभवतः अन्य एनोटेशन) से गणितीय प्रमाण दायित्वों का एक संग्रह उत्पन्न होता है, जिसकी सच्चाई प्रणाली के विनिर्देशों के अनुरूप होती है, और इन दायित्वों का निर्वहन या तो प्रूफ सहायकों (इंटरैक्टिव प्रमेय प्रोवर्स) का उपयोग करते हुए होता है ( जैसे कि HOL प्रमेय सिद्ध, [[ ACL2 ]], इसाबेल (प्रमेय सिद्ध), [[ Coq ]] या [[ प्रोटोटाइप सत्यापन प्रणाली ]]), या स्वचालित प्रमेय सिद्ध, विशेष रूप से संतुष्टि मोडुलो सिद्धांत (SMT) सॉल्वर सहित। इस दृष्टिकोण का नुकसान यह है कि इसके लिए उपयोगकर्ता को विस्तार से समझने की आवश्यकता हो सकती है कि प्रणाली सही तरीके से क्यों काम करता है, और इस जानकारी को सत्यापन प्रणाली तक पहुंचाने के लिए, या तो प्रमेयों के अनुक्रम के रूप में या विनिर्देशों के रूप में ( प्रणाली घटकों (जैसे कार्य या प्रक्रियाएं) और शायद उप-घटक (जैसे लूप या डेटा संरचनाएं) के अपरिवर्तनीय, पूर्व शर्त, पोस्टकंडिशन)। | ||
| Line 22: | Line 22: | ||
=== सॉफ्टवेयर === | === सॉफ्टवेयर === | ||
सॉफ्टवेयर प्रोग्राम के औपचारिक सत्यापन में यह प्रमाणित करना | सॉफ्टवेयर प्रोग्राम के औपचारिक सत्यापन में यह प्रमाणित करना सम्मिलित है कि एक प्रोग्राम अपने व्यवहार के औपचारिक विनिर्देश को पूरा करता है। औपचारिक सत्यापन के उपक्षेत्रों में निगमनात्मक सत्यापन (ऊपर देखें), अमूर्त व्याख्या, स्वचालित प्रमेय सिद्ध करना, प्रकार प्रणालियाँ, और औपचारिक विधियाँ#हल्के औपचारिक तरीके सम्मिलित हैं। एक होनहार प्रकार-आधारित सत्यापन दृष्टिकोण निर्भर प्रकार है, जिसमें कार्यों के प्रकारों में उन कार्यों के विनिर्देशों (कम से कम भाग) सम्मिलित हैं, और कोड की जाँच करना उन विशिष्टताओं के विरुद्ध इसकी विशुद्धता स्थापित करता है। विशेष मामले के रूप में पूरी तरह से विशेष रुप से टाइप की गई भाषाएं डिडक्टिव वेरिफिकेशन का समर्थन करती हैं। | ||
एक अन्य पूरक दृष्टिकोण प्रोग्राम व्युत्पत्ति है, जिसमें विशुद्धता-संरक्षण चरणों की एक श्रृंखला द्वारा [[ कार्यात्मक प्रोग्रामिंग ]] विनिर्देशों से कुशल कोड का उत्पादन किया जाता है। इस दृष्टिकोण का एक उदाहरण बर्ड-मीर्टेंस औपचारिकता है, और इस दृष्टिकोण को [[ निर्माण द्वारा सही ]] के रूप में देखा जा सकता है। | एक अन्य पूरक दृष्टिकोण प्रोग्राम व्युत्पत्ति है, जिसमें विशुद्धता-संरक्षण चरणों की एक श्रृंखला द्वारा [[ कार्यात्मक प्रोग्रामिंग ]] विनिर्देशों से कुशल कोड का उत्पादन किया जाता है। इस दृष्टिकोण का एक उदाहरण बर्ड-मीर्टेंस औपचारिकता है, और इस दृष्टिकोण को [[ निर्माण द्वारा सही ]] के रूप में देखा जा सकता है। | ||
ये तकनीकें सु[[ दृढ़ता ]] हो सकती हैं, जिसका अर्थ है कि सत्यापित गुणों को शब्दार्थ से तार्किक रूप से निकाला जा सकता है, या असंदिग्ध, जिसका अर्थ है कि ऐसी कोई गारंटी नहीं है। एक ध्वनि तकनीक तभी परिणाम देती है जब वह संभावनाओं के पूरे स्थान को कवर कर लेती है। एक गलत तकनीक का एक उदाहरण वह है जो संभावनाओं के केवल एक सबसेट को | ये तकनीकें सु[[ दृढ़ता ]] हो सकती हैं, जिसका अर्थ है कि सत्यापित गुणों को शब्दार्थ से तार्किक रूप से निकाला जा सकता है, या असंदिग्ध, जिसका अर्थ है कि ऐसी कोई गारंटी नहीं है। एक ध्वनि तकनीक तभी परिणाम देती है जब वह संभावनाओं के पूरे स्थान को कवर कर लेती है। एक गलत तकनीक का एक उदाहरण वह है जो संभावनाओं के केवल एक सबसेट को सम्मिलित करता है, उदाहरण के लिए केवल एक निश्चित संख्या तक पूर्णांक, और एक अच्छा-पर्याप्त परिणाम देता है। तकनीकें [[ निर्णायकता (तर्क) ]] भी हो सकती हैं, जिसका अर्थ है कि उनके एल्गोरिथम कार्यान्वयन एक उत्तर के साथ [[ समाप्ति विश्लेषण ]] हैं, या अनिर्णीत हैं, जिसका अर्थ है कि वे कभी भी समाप्त नहीं हो सकते हैं। संभावनाओं के दायरे को सीमित करके, कोई भी निर्णायक ध्वनि तकनीक उपलब्ध नहीं होने पर अस्वास्थ्यकर तकनीकों का निर्माण किया जा सकता है। | ||
== सत्यापन और सत्यापन == | == सत्यापन और सत्यापन == | ||
| Line 35: | Line 35: | ||
* सत्यापन: क्या हमने वह बनाया है जो हम बनाने की कोशिश कर रहे थे? , यानी, उत्पाद विनिर्देशों के अनुरूप है? | * सत्यापन: क्या हमने वह बनाया है जो हम बनाने की कोशिश कर रहे थे? , यानी, उत्पाद विनिर्देशों के अनुरूप है? | ||
सत्यापन प्रक्रिया में स्थिर/संरचनात्मक और गतिशील/व्यवहारिक पहलू | सत्यापन प्रक्रिया में स्थिर/संरचनात्मक और गतिशील/व्यवहारिक पहलू सम्मिलित हैं। [[ उदाहरण ]] के लिए, एक सॉफ्टवेयर उत्पाद के लिए कोई स्रोत कोड (स्थैतिक) का निरीक्षण कर सकता है और विशिष्ट परीक्षण मामलों (गतिशील) के खिलाफ चल सकता है। सत्यापन आमतौर पर केवल गतिशील रूप से किया जा सकता है, अर्थात, उत्पाद को विशिष्ट और असामान्य उपयोगों के माध्यम से रखकर परीक्षण किया जाता है (क्या यह संतोषजनक रूप से सभी उपयोग मामलों को पूरा करता है?)। | ||
== स्वचालित कार्यक्रम की मरम्मत == | == स्वचालित कार्यक्रम की मरम्मत == | ||
{{main|Automatic bug fixing}} | {{main|Automatic bug fixing}} | ||
प्रोग्राम की मरम्मत [[ ओरेकल (कम्प्यूटेबिलिटी) ]] के संबंध में की जाती है, जिसमें प्रोग्राम की वांछित कार्यक्षमता | प्रोग्राम की मरम्मत [[ ओरेकल (कम्प्यूटेबिलिटी) ]] के संबंध में की जाती है, जिसमें प्रोग्राम की वांछित कार्यक्षमता सम्मिलित होती है जिसका उपयोग जेनरेट किए गए फिक्स के सत्यापन के लिए किया जाता है। एक सरल उदाहरण एक टेस्ट-सूट है- इनपुट/आउटपुट जोड़े प्रोग्राम की कार्यक्षमता निर्दिष्ट करते हैं। विभिन्न प्रकार की तकनीकों को नियोजित किया जाता है, विशेष रूप से संतुष्टि मॉडुलो सिद्धांतों (एसएमटी) सॉल्वरों का उपयोग करते हुए,<ref>{{Cite book|title = बग्गी की स्वचालित मरम्मत यदि स्थितियाँ और एसएमटी के साथ पूर्व शर्त नहीं हैं|author1=Favio DeMarco |author2=Jifeng Xuan |author3=Daniel Le Berre |author4=Martin Monperrus |date = 2014|journal = Proceedings of the 6th International Workshop on Constraints in Software Testing, Verification, and Analysis (CSTVA 2014)|pages = 30–39|doi = 10.1145/2593735.2593740|arxiv = 1404.3186|isbn = 9781450328470|s2cid=506586 }}</ref> और [[ आनुवंशिक प्रोग्रामिंग ]],<ref>{{cite journal |last1=Le Goues |first1=Claire |last2=Nguyen |first2=ThanhVu |last3=Forrest |first3=Stephanie |last4=Weimer |first4=Westley |title=GenProg: स्वचालित सॉफ़्टवेयर मरम्मत के लिए एक सामान्य विधि|journal=IEEE Transactions on Software Engineering |date=January 2012 |volume=38 |issue=1 |pages=54–72 |doi=10.1109/TSE.2011.104 |s2cid=4111307 |url = http://search.proquest.com/openview/f837f11066e9c9552df9e497064d6d80/1?pq-origsite=gscholar&cbl=21418&casa_token=X2fQSRNgLNwAAAAA:CBjvmrcBLZRqV7kjC-MY74s0wF68lhBvLF6rV4DWZkalzo2KdlUUzuMU38YgSmXGbwEL2NAr4w}}</ref> फिक्स के लिए संभावित उम्मीदवारों को उत्पन्न करने और उनका मूल्यांकन करने के लिए विकासवादी कंप्यूटिंग का उपयोग करना। पूर्व पद्धति नियतात्मक है, जबकि बाद वाली यादृच्छिक है। | ||
कार्यक्रम की मरम्मत औपचारिक सत्यापन और [[ कार्यक्रम संश्लेषण ]] की तकनीकों को जोड़ती है। औपचारिक सत्यापन में दोष-स्थानीयकरण तकनीकों का उपयोग प्रोग्राम बिंदुओं की गणना करने के लिए किया जाता है जो संभावित बग-स्थान हो सकते हैं, जिन्हें संश्लेषण मॉड्यूल द्वारा लक्षित किया जा सकता है। खोज स्थान को कम करने के लिए मरम्मत प्रणालियां अधिकांशतः बग के एक छोटे पूर्व-निर्धारित वर्ग पर ध्यान केंद्रित करती हैं। मौजूदा तकनीकों की कम्प्यूटेशनल लागत के कारण औद्योगिक उपयोग सीमित है। | कार्यक्रम की मरम्मत औपचारिक सत्यापन और [[ कार्यक्रम संश्लेषण ]] की तकनीकों को जोड़ती है। औपचारिक सत्यापन में दोष-स्थानीयकरण तकनीकों का उपयोग प्रोग्राम बिंदुओं की गणना करने के लिए किया जाता है जो संभावित बग-स्थान हो सकते हैं, जिन्हें संश्लेषण मॉड्यूल द्वारा लक्षित किया जा सकता है। खोज स्थान को कम करने के लिए मरम्मत प्रणालियां अधिकांशतः बग के एक छोटे पूर्व-निर्धारित वर्ग पर ध्यान केंद्रित करती हैं। मौजूदा तकनीकों की कम्प्यूटेशनल लागत के कारण औद्योगिक उपयोग सीमित है। | ||
| Line 52: | Line 52: | ||
[http://www.ganssle.com/rants/gettingitright.htm "Getting it Right"] by Jack Ganssle</ref> | [http://www.ganssle.com/rants/gettingitright.htm "Getting it Right"] by Jack Ganssle</ref> | ||
2016 में, येल में झोंग शाओ के नेतृत्व में एक टीम ने CertiKOS नामक एक औपचारिक रूप से सत्यापित ऑपरेटिंग प्रणाली कर्नेल विकसित किया।<ref>{{cite web|url=https://www.zdnet.com/article/certikos-a-hacker-proof-os/|title=हैक नहीं किया जा सकने वाला OS? CertiKOS सुरक्षित सिस्टम कर्नेल के निर्माण को सक्षम करता है|first=Robin|last=Harris|website=ZDNet|access-date=June 10, 2019}}</ref><ref>{{cite web|url=https://www.ibtimes.co.uk/certikos-yale-develops-worlds-first-hacker-resistant-operating-system-1591712|title=CertiKOS: येल ने दुनिया का पहला हैकर प्रतिरोधी ऑपरेटिंग सिस्टम विकसित किया है|date=November 15, 2016|website=International Business Times UK|access-date=June 10, 2019}}</ref> | 2016 में, येल में झोंग शाओ के नेतृत्व में एक टीम ने CertiKOS नामक एक औपचारिक रूप से सत्यापित ऑपरेटिंग प्रणाली कर्नेल विकसित किया।<ref>{{cite web|url=https://www.zdnet.com/article/certikos-a-hacker-proof-os/|title=हैक नहीं किया जा सकने वाला OS? CertiKOS सुरक्षित सिस्टम कर्नेल के निर्माण को सक्षम करता है|first=Robin|last=Harris|website=ZDNet|access-date=June 10, 2019}}</ref><ref>{{cite web|url=https://www.ibtimes.co.uk/certikos-yale-develops-worlds-first-hacker-resistant-operating-system-1591712|title=CertiKOS: येल ने दुनिया का पहला हैकर प्रतिरोधी ऑपरेटिंग सिस्टम विकसित किया है|date=November 15, 2016|website=International Business Times UK|access-date=June 10, 2019}}</ref> | ||
2017 तक, नेटवर्क के गणितीय प्रतिरूप के माध्यम से बड़े कंप्यूटर नेटवर्क के डिजाइन के लिए औपचारिक सत्यापन लागू किया गया है,<ref>{{cite web|last=Scroxton|first=Alex|title=सिस्को के लिए, आशय-आधारित नेटवर्किंग भविष्य की तकनीकी मांगों की शुरुआत करती है|url=http://www.computerweekly.com/news/252434028/For-Cisco-intent-based-networking-heralds-future-tech-demands|publisher=Computer Weekly|access-date=February 12, 2018}}</ref> और एक नई नेटवर्क प्रौद्योगिकी श्रेणी, आशय-आधारित नेटवर्किंग के हिस्से के रूप में।<ref>{{cite web|last=Lerner|first=Andrew|title=आशय आधारित नेटवर्किंग|url=https://blogs.gartner.com/andrew-lerner/2017/02/07/intent-based-networking/|publisher=Gartner|access-date=February 12, 2018}}</ref> औपचारिक सत्यापन समाधान प्रदान करने वाले नेटवर्क सॉफ़्टवेयर विक्रेताओं में [[ सिस्को ]] | 2017 तक, नेटवर्क के गणितीय प्रतिरूप के माध्यम से बड़े कंप्यूटर नेटवर्क के डिजाइन के लिए औपचारिक सत्यापन लागू किया गया है,<ref>{{cite web|last=Scroxton|first=Alex|title=सिस्को के लिए, आशय-आधारित नेटवर्किंग भविष्य की तकनीकी मांगों की शुरुआत करती है|url=http://www.computerweekly.com/news/252434028/For-Cisco-intent-based-networking-heralds-future-tech-demands|publisher=Computer Weekly|access-date=February 12, 2018}}</ref> और एक नई नेटवर्क प्रौद्योगिकी श्रेणी, आशय-आधारित नेटवर्किंग के हिस्से के रूप में।<ref>{{cite web|last=Lerner|first=Andrew|title=आशय आधारित नेटवर्किंग|url=https://blogs.gartner.com/andrew-lerner/2017/02/07/intent-based-networking/|publisher=Gartner|access-date=February 12, 2018}}</ref> औपचारिक सत्यापन समाधान प्रदान करने वाले नेटवर्क सॉफ़्टवेयर विक्रेताओं में [[ सिस्को ]] सम्मिलित है<ref>{{cite web|last=Kerravala|first=Zeus|title=सिस्को इंटेंट आधारित नेटवर्क को डेटा सेंटर में लाता है|url=https://www.networkworld.com/article/3252804/data-center/cisco-brings-intent-based-networks-to-the-data-center.html|publisher=NetworkWorld|access-date=February 12, 2018}}</ref> फॉरवर्ड नेटवर्क<ref>{{cite web|title=फॉरवर्ड नेटवर्क: त्वरित और डी-जोखिम नेटवर्क संचालन|url=http://www.insightssuccess.com/forward-networks-accelerating-de-risking-network-operations/|publisher=Insights Success|access-date=February 12, 2018}}</ref><ref>{{cite web|title=इंटेंट = आधारित नेटवर्किंग में ग्राउंडेड होना|url=https://images.idgesg.net/assets/2018/01/idg_2018_intent-based_networking.pdf|publisher=NetworkWorld|access-date=February 12, 2018}}</ref> और वेरिफ्लो प्रणाली ्स।<ref>{{cite web|title=वेरिफ्लो सिस्टम्स|url=https://www.bloomberg.com/research/stocks/private/snapshot.asp?privcapid=274750862|publisher=Bloomberg|access-date=February 12, 2018}}</ref> | ||
[[ स्पार्क (प्रोग्रामिंग भाषा) ]] एक टूलसेट प्रदान करता है जो औपचारिक सत्यापन के साथ सॉफ्टवेयर विकास को सक्षम बनाता है और स्पार्क (प्रोग्रामिंग भाषा)#औद्योगिक अनुप्रयोग|कई उच्च-अखंडता प्रणालियों में उपयोग किया जाता है।{{cn|date=October 2022}} | [[ स्पार्क (प्रोग्रामिंग भाषा) ]] एक टूलसेट प्रदान करता है जो औपचारिक सत्यापन के साथ सॉफ्टवेयर विकास को सक्षम बनाता है और स्पार्क (प्रोग्रामिंग भाषा)#औद्योगिक अनुप्रयोग|कई उच्च-अखंडता प्रणालियों में उपयोग किया जाता है।{{cn|date=October 2022}} | ||
[[ CompCert ]] एक औपचारिक रूप से सत्यापित C संकलक है जो अधिकांश ISO C को लागू करता है।{{cn|date=October 2022}} | [[ CompCert ]] एक औपचारिक रूप से सत्यापित C संकलक है जो अधिकांश ISO C को लागू करता है।{{cn|date=October 2022}} | ||
| Line 68: | Line 68: | ||
* सैद्धांतिक कंप्यूटर विज्ञान में महत्वपूर्ण प्रकाशनों की सूची #औपचारिक सत्यापन | * सैद्धांतिक कंप्यूटर विज्ञान में महत्वपूर्ण प्रकाशनों की सूची #औपचारिक सत्यापन | ||
* स्टेटिक कोड विश्लेषण | * स्टेटिक कोड विश्लेषण | ||
* [[ परिमित-राज्य सत्यापन में अस्थायी तर्क ]] | * [[ परिमित-राज्य सत्यापन में अस्थायी तर्क | परिमित-स्थिति सत्यापन में अस्थायी तर्क]] | ||
* [[ पोस्ट-सिलिकॉन सत्यापन ]] | * [[ पोस्ट-सिलिकॉन सत्यापन ]] | ||
* [[ बुद्धिमान सत्यापन ]] | * [[ बुद्धिमान सत्यापन ]] | ||
Revision as of 13:24, 9 December 2022
 | This article needs additional citations for verification. (जून 2009) (Learn how and when to remove this template message) |
हार्डवेयर और सॉफ्टवेयर प्रणाली के संदर्भ में, औपचारिक सत्यापन गणित के औपचारिक विधियों का उपयोग करके एक निश्चित औपचारिक विनिर्देश या सामग्री के संबंध में एक प्रणाली के अंतर्निहित कलन विधि के गणितये प्रमाण की विशुद्धता को स्वीकार करने या अस्वीकार करने का कार्य है।[1]
यह औपचारिक सत्यापन प्रणाली की विशुद्धता को प्रमाणित करने में सहायक हो सकता है जैसे: क्रिप्टोग्राफिक प्रोटोकॉल , संयोजन तर्क , आंतरिक मेमोरी के साथ डिजिटल सर्किट और स्रोत कोड के रूप में व्यक्त सॉफ़्टवेयर।
इन प्रणालियों का सत्यापन प्रणाली के एक संक्षिप्त गणितीय प्रतिरूप पर एक औपचारिक प्रमाण प्रदान करके किया जाता है, गणितीय प्रतिरूप और प्रणाली की प्रकृति के मध्य पत्राचार को इसके अतिरिक्त निर्माण द्वारा जाना जाता है। गणितीय वस्तुओं के उदाहरण अधिकांशतः प्रतिरूप प्रणाली के लिए उपयोग किए जाते हैं: परिमित-स्थिति मशीनें, लेबल संक्रमण प्रणाली , पेट्री नेट , सदिश जोड़ प्रणाली , समयबद्ध ऑटोमेटन, हाइब्रिड ऑटोमेटा , प्रक्रिया बीजगणित , प्रोग्रामिंग भाषाओं के औपचारिक शब्दार्थ जैसे परिचालन शब्दार्थ , अर्थ शब्दार्थ, स्वयंसिद्ध शब्दार्थ और होरे तर्क ।[2]
दृष्टिकोण
यह एक दृष्टिकोण और गठन प्रतिरूप की जाँच है, जिसमें गणितीय प्रतिरूप का एक व्यवस्थित रूप से संपूर्ण अन्वेषण सम्मिलित है (यह परिमित प्रतिरूप सिद्धांत के लिए संभव है, लेकिन कुछ अनंत प्रतिरूप के लिए भी है जहाँ स्थितों के अनंत अवयवों को अमूर्तता का उपयोग करके या लाभ उठाकर प्रभावी विधियों से प्रदर्शित किया जा सकता है। आमतौर पर, इसमें एक ही ऑपरेशन में स्थितिों के पूरे समूह पर विचार करने और कंप्यूटिंग समय को कम करने के लिए स्मार्ट और डोमेन-विशिष्ट अमूर्त तकनीकों का उपयोग करके प्रतिरूप में सभी स्थितिों और संक्रमणों की खोज करना सम्मिलित है। कार्यान्वयन तकनीकों में स्थिति अंतरिक्ष गणना , प्रतीकात्मक स्थिति अंतरिक्ष गणना, सार व्याख्या , प्रतीकात्मक अनुकरण , अमूर्त शोधन सम्मिलित हैं।[citation needed] सत्यापित किए जाने वाले गुणों को अधिकांशतः लौकिक तर्क ्स में वर्णित किया जाता है, जैसे रैखिक लौकिक तर्क (एलटीएल), संपत्ति विशिष्टता भाषा (पीएसएल), प्रणाली वेरिलॉग एसेर्शन (एसवीए),[3] या कम्प्यूटेशनल वृक्ष तर्क (CTL)। प्रतिरूप जाँच का बड़ा फायदा यह है कि यह अधिकांशतः पूरी तरह से स्वचालित होती है; इसका प्राथमिक नुकसान यह है कि यह सामान्य रूप से बड़ी प्रणालियों के पैमाने पर नहीं होता है; प्रतीकात्मक प्रतिरूप आमतौर पर स्थिति के कुछ सौ बिट्स तक सीमित होते हैं, जबकि स्पष्ट स्थिति गणना के लिए अपेक्षाकृत छोटे होने के लिए स्थिति स्थान की खोज की आवश्यकता होती है।
एक अन्य दृष्टिकोण कटौतीत्मक सत्यापन है। इसमें प्रणाली और इसकी विशिष्टताओं (और संभवतः अन्य एनोटेशन) से गणितीय प्रमाण दायित्वों का एक संग्रह उत्पन्न होता है, जिसकी सच्चाई प्रणाली के विनिर्देशों के अनुरूप होती है, और इन दायित्वों का निर्वहन या तो प्रूफ सहायकों (इंटरैक्टिव प्रमेय प्रोवर्स) का उपयोग करते हुए होता है ( जैसे कि HOL प्रमेय सिद्ध, ACL2 , इसाबेल (प्रमेय सिद्ध), Coq या प्रोटोटाइप सत्यापन प्रणाली ), या स्वचालित प्रमेय सिद्ध, विशेष रूप से संतुष्टि मोडुलो सिद्धांत (SMT) सॉल्वर सहित। इस दृष्टिकोण का नुकसान यह है कि इसके लिए उपयोगकर्ता को विस्तार से समझने की आवश्यकता हो सकती है कि प्रणाली सही तरीके से क्यों काम करता है, और इस जानकारी को सत्यापन प्रणाली तक पहुंचाने के लिए, या तो प्रमेयों के अनुक्रम के रूप में या विनिर्देशों के रूप में ( प्रणाली घटकों (जैसे कार्य या प्रक्रियाएं) और शायद उप-घटक (जैसे लूप या डेटा संरचनाएं) के अपरिवर्तनीय, पूर्व शर्त, पोस्टकंडिशन)।
सॉफ्टवेयर
सॉफ्टवेयर प्रोग्राम के औपचारिक सत्यापन में यह प्रमाणित करना सम्मिलित है कि एक प्रोग्राम अपने व्यवहार के औपचारिक विनिर्देश को पूरा करता है। औपचारिक सत्यापन के उपक्षेत्रों में निगमनात्मक सत्यापन (ऊपर देखें), अमूर्त व्याख्या, स्वचालित प्रमेय सिद्ध करना, प्रकार प्रणालियाँ, और औपचारिक विधियाँ#हल्के औपचारिक तरीके सम्मिलित हैं। एक होनहार प्रकार-आधारित सत्यापन दृष्टिकोण निर्भर प्रकार है, जिसमें कार्यों के प्रकारों में उन कार्यों के विनिर्देशों (कम से कम भाग) सम्मिलित हैं, और कोड की जाँच करना उन विशिष्टताओं के विरुद्ध इसकी विशुद्धता स्थापित करता है। विशेष मामले के रूप में पूरी तरह से विशेष रुप से टाइप की गई भाषाएं डिडक्टिव वेरिफिकेशन का समर्थन करती हैं।
एक अन्य पूरक दृष्टिकोण प्रोग्राम व्युत्पत्ति है, जिसमें विशुद्धता-संरक्षण चरणों की एक श्रृंखला द्वारा कार्यात्मक प्रोग्रामिंग विनिर्देशों से कुशल कोड का उत्पादन किया जाता है। इस दृष्टिकोण का एक उदाहरण बर्ड-मीर्टेंस औपचारिकता है, और इस दृष्टिकोण को निर्माण द्वारा सही के रूप में देखा जा सकता है।
ये तकनीकें सुदृढ़ता हो सकती हैं, जिसका अर्थ है कि सत्यापित गुणों को शब्दार्थ से तार्किक रूप से निकाला जा सकता है, या असंदिग्ध, जिसका अर्थ है कि ऐसी कोई गारंटी नहीं है। एक ध्वनि तकनीक तभी परिणाम देती है जब वह संभावनाओं के पूरे स्थान को कवर कर लेती है। एक गलत तकनीक का एक उदाहरण वह है जो संभावनाओं के केवल एक सबसेट को सम्मिलित करता है, उदाहरण के लिए केवल एक निश्चित संख्या तक पूर्णांक, और एक अच्छा-पर्याप्त परिणाम देता है। तकनीकें निर्णायकता (तर्क) भी हो सकती हैं, जिसका अर्थ है कि उनके एल्गोरिथम कार्यान्वयन एक उत्तर के साथ समाप्ति विश्लेषण हैं, या अनिर्णीत हैं, जिसका अर्थ है कि वे कभी भी समाप्त नहीं हो सकते हैं। संभावनाओं के दायरे को सीमित करके, कोई भी निर्णायक ध्वनि तकनीक उपलब्ध नहीं होने पर अस्वास्थ्यकर तकनीकों का निर्माण किया जा सकता है।
सत्यापन और सत्यापन
सत्यापन और सत्यापन उद्देश्य के लिए किसी उत्पाद की फिटनेस के परीक्षण का एक पहलू है। मान्यता पूरक पहलू है। अधिकांशतः एक समग्र जाँच प्रक्रिया को सत्यापन और सत्यापन | वी एंड वी के रूप में संदर्भित करता है।
- मान्यता: क्या हम सही चीज़ बनाने की कोशिश कर रहे हैं? , यानी, उत्पाद उपयोगकर्ता की वास्तविक जरूरतों के लिए निर्दिष्ट है?
- सत्यापन: क्या हमने वह बनाया है जो हम बनाने की कोशिश कर रहे थे? , यानी, उत्पाद विनिर्देशों के अनुरूप है?
सत्यापन प्रक्रिया में स्थिर/संरचनात्मक और गतिशील/व्यवहारिक पहलू सम्मिलित हैं। उदाहरण के लिए, एक सॉफ्टवेयर उत्पाद के लिए कोई स्रोत कोड (स्थैतिक) का निरीक्षण कर सकता है और विशिष्ट परीक्षण मामलों (गतिशील) के खिलाफ चल सकता है। सत्यापन आमतौर पर केवल गतिशील रूप से किया जा सकता है, अर्थात, उत्पाद को विशिष्ट और असामान्य उपयोगों के माध्यम से रखकर परीक्षण किया जाता है (क्या यह संतोषजनक रूप से सभी उपयोग मामलों को पूरा करता है?)।
स्वचालित कार्यक्रम की मरम्मत
प्रोग्राम की मरम्मत ओरेकल (कम्प्यूटेबिलिटी) के संबंध में की जाती है, जिसमें प्रोग्राम की वांछित कार्यक्षमता सम्मिलित होती है जिसका उपयोग जेनरेट किए गए फिक्स के सत्यापन के लिए किया जाता है। एक सरल उदाहरण एक टेस्ट-सूट है- इनपुट/आउटपुट जोड़े प्रोग्राम की कार्यक्षमता निर्दिष्ट करते हैं। विभिन्न प्रकार की तकनीकों को नियोजित किया जाता है, विशेष रूप से संतुष्टि मॉडुलो सिद्धांतों (एसएमटी) सॉल्वरों का उपयोग करते हुए,[4] और आनुवंशिक प्रोग्रामिंग ,[5] फिक्स के लिए संभावित उम्मीदवारों को उत्पन्न करने और उनका मूल्यांकन करने के लिए विकासवादी कंप्यूटिंग का उपयोग करना। पूर्व पद्धति नियतात्मक है, जबकि बाद वाली यादृच्छिक है।
कार्यक्रम की मरम्मत औपचारिक सत्यापन और कार्यक्रम संश्लेषण की तकनीकों को जोड़ती है। औपचारिक सत्यापन में दोष-स्थानीयकरण तकनीकों का उपयोग प्रोग्राम बिंदुओं की गणना करने के लिए किया जाता है जो संभावित बग-स्थान हो सकते हैं, जिन्हें संश्लेषण मॉड्यूल द्वारा लक्षित किया जा सकता है। खोज स्थान को कम करने के लिए मरम्मत प्रणालियां अधिकांशतः बग के एक छोटे पूर्व-निर्धारित वर्ग पर ध्यान केंद्रित करती हैं। मौजूदा तकनीकों की कम्प्यूटेशनल लागत के कारण औद्योगिक उपयोग सीमित है।
उद्योग उपयोग
 | This section may require cleanup to meet Wikipedia's quality standards. The specific problem is: needs a more well-rounded overview of the subject; filter for what is actually used in industry; only mention notable papers. (October 2022) (Learn how and when to remove this template message) |
डिजाइनों की जटिलता में वृद्धि हार्डवेयर उद्योग में औपचारिक सत्यापन तकनीकों के महत्व को बढ़ाती है।[6][7] वर्तमान में, अधिकांश या सभी प्रमुख हार्डवेयर कंपनियों द्वारा औपचारिक सत्यापन का उपयोग किया जाता है,[8] लेकिन सॉफ्टवेयर उद्योग में इसका उपयोग अभी भी कम हो रहा है।[citation needed] इसे हार्डवेयर उद्योग में अधिक आवश्यकता के लिए जिम्मेदार ठहराया जा सकता है, जहां त्रुटियों का व्यावसायिक महत्व अधिक होता है।[citation needed] घटकों के बीच संभावित सूक्ष्म अंतःक्रियाओं के कारण, सिमुलेशन द्वारा संभावनाओं के यथार्थवादी सेट का प्रयोग करना कठिन होता जा रहा है। हार्डवेयर डिजाइन के महत्वपूर्ण पहलू स्वचालित प्रूफ विधियों के लिए उत्तरदायी हैं, औपचारिक सत्यापन को शुरू करना आसान और अधिक उत्पादक बनाते हैं।[9]
As of 2011[update], कई ऑपरेटिंग प्रणाली औपचारिक रूप से सत्यापित किए गए हैं: NICTA का सुरक्षित L4 माइक्रोकर्नेल परिवार # न्यू साउथ वेल्स विश्वविद्यालय और NICTA, OK लैब्स द्वारा seL4 के रूप में व्यावसायिक रूप से बेचा गया;[10] पूर्वी चीन सामान्य विश्वविद्यालय द्वारा OSEK/VDX आधारित रीयल-टाइम ऑपरेटिंग प्रणाली ORIENTAIS;[citation needed] ग्रीन हिल्स सॉफ्टवेयर की वफ़ादारी (ऑपरेटिंग प्रणाली );[citation needed] और SYSGO का PikeOS ।[11][12] 2016 में, येल में झोंग शाओ के नेतृत्व में एक टीम ने CertiKOS नामक एक औपचारिक रूप से सत्यापित ऑपरेटिंग प्रणाली कर्नेल विकसित किया।[13][14] 2017 तक, नेटवर्क के गणितीय प्रतिरूप के माध्यम से बड़े कंप्यूटर नेटवर्क के डिजाइन के लिए औपचारिक सत्यापन लागू किया गया है,[15] और एक नई नेटवर्क प्रौद्योगिकी श्रेणी, आशय-आधारित नेटवर्किंग के हिस्से के रूप में।[16] औपचारिक सत्यापन समाधान प्रदान करने वाले नेटवर्क सॉफ़्टवेयर विक्रेताओं में सिस्को सम्मिलित है[17] फॉरवर्ड नेटवर्क[18][19] और वेरिफ्लो प्रणाली ्स।[20] स्पार्क (प्रोग्रामिंग भाषा) एक टूलसेट प्रदान करता है जो औपचारिक सत्यापन के साथ सॉफ्टवेयर विकास को सक्षम बनाता है और स्पार्क (प्रोग्रामिंग भाषा)#औद्योगिक अनुप्रयोग|कई उच्च-अखंडता प्रणालियों में उपयोग किया जाता है।[citation needed] CompCert एक औपचारिक रूप से सत्यापित C संकलक है जो अधिकांश ISO C को लागू करता है।[citation needed]
यह भी देखें
- स्वचालित प्रमेय प्रमाणित करना
- प्रतिरूप जाँच
- प्रतिरूप जाँच उपकरणों की सूची
- औपचारिक तुल्यता जाँच
- सबूत चेकर
- संपत्ति विशिष्टता भाषा
- सैद्धांतिक कंप्यूटर विज्ञान में महत्वपूर्ण प्रकाशनों की सूची #औपचारिक सत्यापन
- स्टेटिक कोड विश्लेषण
- परिमित-स्थिति सत्यापन में अस्थायी तर्क
- पोस्ट-सिलिकॉन सत्यापन
- बुद्धिमान सत्यापन
- रनटाइम सत्यापन
इस पेज में लापता आंतरिक लिंक की सूची
- अंक शास्त्र
- औपचारिक तरीके
- गणित का प्रतिरूप
- सोर्स कोड
- परिमित अवस्था मशीन
- सांकेतिक शब्दार्थ
- समयबद्ध automaton
- संतुष्टि मॉड्यूल सिद्धांत
- स्वचालित प्रमेय प्रमाणित करना
- एचओएल प्रमेय समर्थक
- इसाबेल (सिद्धांत प्रमाणित करें)
- सबूत सहायक
- कार्यक्रम व्युत्पत्ति
- प्रकार प्रणाली
- आश्रित प्रकार
- जाँच और वैधता
- अखंडता (ऑपरेटिंग प्रणाली )
- स्थैतिक कोड विश्लेषण
संदर्भ
- ↑ 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.
