औपचारिक पद्यतियां: Difference between revisions

Revision as of 08:56, 21 October 2022

कंप्यूटर विज्ञान में, सॉफ़्टवेयर और संगणक धातु सामग्री, हार्डवेयर सिस्टम की विशिष्टता, विकास के औपचारिक सत्यापन के लिए गणित की कठोर तकनीकें हैं।^[1] सॉफ्टवेयर और हार्डवेयर डिजाइन के लिए औपचारिक तरीकों का उपयोग इस उम्मीद से प्रेरित है कि,अन्य इंजीनियरिंग विषयों की तरह, उपयुक्त गणितीय विश्लेषण करने से डिजाइन की विश्वसनीयता और मजबूती में योगदान हो सकता है।^[2] औपचारिक विधियों में कंप्यूटर विज्ञान की गणना,विभिन्न प्रकार के सैद्धांतिक कंप्यूटर विज्ञान के मूल सिद्धांतों को नियोजित करती हैं, जिनमें औपचारिक भाषा, ऑटोमेटा सिद्धांत, नियंत्रण सिद्धांत ,कार्यक्रम शब्दार्थ , प्रकार प्रणाली और प्रकार सिद्धांत में तर्क सहित विभिन्न बुनियादी बातों का उपयोग किया जाता है।^[3]

पृष्ठभूमि

अर्ध-औपचारिक तरीके औपचारिकता और भाषाएं हैं जिन्हें पूरी तरह से "औपचारिक" नहीं माना जाता है। यह शब्दार्थ को बाद के चरण में पूरा करने के कार्य को स्थगित करता है, जो बाद में या तो मानव व्याख्या द्वारा या कोड या टेस्ट केस जनरेटर जैसे सॉफ़्टवेयर के माध्यम से व्याख्या द्वारा किया जाता है।^[4]

वर्गीकरण

औपचारिक तरीकों का इस्तेमाल कई स्तरों पर किया जा सकता है:

स्तर 0: औपचारिक विनिर्देश शुरू करके और फिर अनौपचारिक रूप से इससे एक कार्यक्रम विकसित किया जा सकता है। इसे 'औपचारिक तरीके लाइट' करार दिया गया है। यह कई मामलों में सबसे कम लागत विकल्प हो सकता है।

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

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

इसके बारे में अधिक जानकारी नीचे दी गई है।

प्रोग्रामिंग भाषाओं के औपचारिक शब्दार्थ के साथ, औपचारिक विधियों की शैलियों को मोटे तौर पर निम्नानुसार वर्गीकृत किया जा सकता है:

सांकेतिक शब्दार्थ, जिसमें एक प्रणाली का अर्थ डोमेन सिद्धांत के गणितीय सिद्धांत में व्यक्त किया जाता है। इस तरह के तरीकों के समर्थक सिस्टम को अर्थ देने के लिए डोमेन की अच्छी तरह से समझी गई प्रकृति पर भरोसा करते हैं; आलोचकों का कहना है कि हर प्रणाली को सहज या स्वाभाविक रूप से एक कार्य के रूप में नहीं देखा जा सकता है। ऐसी विधियों के समर्थक सिस्टम को अर्थ देने के लिए डोमेन को अच्छी तरह से समझ कर ही उसकी प्रकृति पर भरोसा करते हैं;
परिचालन शब्दार्थ , जिसमें एक सिस्टम का अर्थ एक (संभवतः) सरल कम्प्यूटेशनल मॉडल की क्रियाओं के अनुक्रम के रूप में व्यक्त किया जाता है। इस तरह के तरीकों के समर्थक अपने मॉडल की सादगी को अभिव्यक्तिपूर्ण स्पष्टता के साधन के रूप में इंगित करते हैं; आलोचकों का कहना है कि शब्दार्थ की समस्या में अभी देरी हुई है (जो सरल मॉडल के शब्दार्थ को परिभाषित करता है?) इस तरह के तरीकों के समर्थक अपने मॉडल की सादगी को अभिव्यक्तिपूर्ण स्पष्टता के साधन के रूप में इंगित करते हैं;
स्वयंसिद्ध शब्दार्थ , जिसमें सिस्टम का अर्थ पूर्व शर्त और शर्त के बाद के संदर्भ में व्यक्त किया जाता है जो कि सिस्टम द्वारा किसी कार्य को करने से पहले और बाद में एक कार्य करता है। समर्थकों ने शास्त्रीय तर्क के संबंध पर ध्यान दिया; आलोचकों ने ध्यान दिया कि इस तरह के शब्दार्थ वास्तव में कभी भी यह वर्णन नहीं करते हैं कि एक प्रणाली क्या करती है (केवल वही जो पहले और बाद में सच है)।
- Axiomatic semantics, in which the meaning of the system is expressed in terms of preconditions and postconditions which are true before and after the system performs a task, respectively. Proponents note the connection to classical logic; critics note that such semantics never really describe what a system does (merely what is true before and afterwards). पूर्व शर्त और बाद की शर्तें जो क्रमशः सिस्टम द्वारा किसी कार्य को करने से पहले और बाद में सत्य हैं।

हल्के औपचारिक तरीके

कुछ चिकित्सकों का मानना है कि औपचारिक तरीके समुदाय ने एक विनिर्देश या डिजाइन की पूर्ण औपचारिकता पर अधिक जोर दिया है।^[5]^[6] उनका तर्क है कि इसमें शामिल भाषाओं की अभिव्यंजना, साथ ही प्रतिरूपित की जा रही प्रणालियों की जटिलता, पूर्ण औपचारिकता को एक कठिन और महंगा कार्य बनाती है। एक विकल्प के रूप में, विभिन्न हल्के औपचारिक तरीके, जो आंशिक विनिर्देश और केंद्रित अनुप्रयोग पर जोर देते हैं, एक विकल्प के रूप में, प्रस्तावित किए गए हैं। औपचारिक तरीकों के लिए इस हल्के दृष्टिकोण के उदाहरणों में मिश्र धातु भाषा ऑब्जेक्ट मॉडलिंग नोटेशन शामिल है,^[7] Z संकेतन के कुछ पहलुओं का डेनी का संश्लेषण,^[8] उपयोग केस संचालित विकास, और सीएसके वियना विकास विधि टूल्स।^[9]

उपयोग

सॉफ्टवेयर विकास प्रक्रिया के माध्यम से विभिन्न बिंदुओं पर औपचारिक तरीकों को लागू किया जा सकता है।

विशिष्टता

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

औपचारिक विनिर्देश प्रणालियों की आवश्यकता को वर्षों से नोट किया गया है। ALGOL 58 रिपोर्ट में,^[10] जॉन बैकस ने प्रोग्रामिंग लैंग्वेज सिंटैक्स का वर्णन करने के लिए एक औपचारिक संकेतन प्रस्तुत किया, जिसे बाद में बैकस सामान्य रूप नाम दिया गया और फिर इसका नाम बदलकर बैकस-नौर फॉर्म (बीएनएफ) कर दिया गया।^[11] बैकस ने यह भी लिखा है कि वाक्यात्मक रूप से मान्य ALGOL कार्यक्रमों के अर्थ का औपचारिक विवरण रिपोर्ट में शामिल करने के लिए समय पर पूरा नहीं किया गया था।" इसलिए कानूनी कार्यक्रमों के शब्दार्थ का औपचारिक उपचार बाद के पेपर में शामिल किया जाएगा।" यह कभी नहीं दिखाई दिया।

विकास

औपचारिक विकास एक उपकरण समर्थित प्रणाली विकास प्रक्रिया के एक एकीकृत भाग के रूप में औपचारिक तरीकों का उपयोग है।

एक बार औपचारिक विनिर्देश तैयार हो जाने के बाद, विनिर्देश को एक गाइड के रूप में इस्तेमाल किया जा सकता है, जबकि ठोस प्रणाली सॉफ्टवेर डिज़ाइन प्रक्रिया के दौरान विकसित हुआ था (यानी आम तौर पर, सॉफ्टवेयर में महसूस किया जाता है, लेकिन संभावित रूप से हार्डवेयर में भी)। उदाहरण के लिए:

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

सत्यापन

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

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

साइन-ऑफ सत्यापन

साइन-ऑफ सत्यापन एक औपचारिक सत्यापन उपकरण का उपयोग है जो अत्यधिक विश्वसनीय है। ऐसा उपकरण पारंपरिक सत्यापन विधियों को प्रतिस्थापित कर सकता है (उपकरण प्रमाणित भी हो सकता है)।

मानव निर्देशित सबूत

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

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

स्वचालित प्रमाण

इसके विपरीत, स्वचालित साधनों द्वारा ऐसी प्रणालियों की शुद्धता के प्रमाण प्रस्तुत करने में रुचि बढ़ रही है। स्वचालित तकनीक तीन सामान्य श्रेणियों में आती है:

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

कुछ स्वचालित प्रमेय प्रोवर्स को मार्गदर्शन की आवश्यकता होती है कि कौन से गुण काफी रोचक हैं जो आगे बढ़ने के लिए पर्याप्त हैं, जबकि अन्य मानवीय हस्तक्षेप के बिना काम करते हैं। यदि पर्याप्त रूप से सार मॉडल नहीं दिया जाता है, तो मॉडल चेकर्स लाखों अरोचक स्तरों की जाँच में जल्दी से फंस सकते हैं।

ऐसी प्रणालियों के समर्थकों का तर्क है कि परिणामों में मानव-निर्मित प्रमाणों की तुलना में अधिक गणितीय निश्चितता है, क्योंकि सभी अरोचक विवरणों को एल्गोरिथम रूप से सत्यापित किया गया है। ऐसी प्रणालियों का उपयोग करने के लिए आवश्यक प्रशिक्षण भी हाथ से अच्छे गणितीय प्रमाण तैयार करने के लिए आवश्यक प्रशिक्षण से कम है, जिससे तकनीक बहुत से चिकित्सकों के लिए आसान हो जाती है।

आलोचक ध्यान दें कि उनमें से कुछ प्रणालियाँ आकाशवाणी (ओरेकल) मशीनों की तरह हैं: वे सत्य का उच्चारण करती हैं, फिर भी उस सत्य का कोई स्पष्टीकरण नहीं देती हैं। ऐसी प्रणाली में "सत्यापनकर्ता के सत्यापन" की समस्या भी है ; यदि सत्यापन में सहायता करने वाला कार्यक्रम स्वयं अप्रमाणित है, तो उत्पादित परिणामों की सुदृढ़ता पर संदेह करने का कारण हो सकता है। कुछ आधुनिकमॉडल जाँच उपकरण अपने प्रमाण में प्रत्येक चरण का विवरण देते हुए एक "प्रमाण लॉग" उत्पन्न करते हैं, जिससे स्वतंत्र सत्यापन दिए जाने उपयुक्त उपकरण का प्रदर्शन करना संभव हो जाता है।

अमूर्त व्याख्या दृष्टिकोण की मुख्य विशेषता यह है कि यह एक ध्वनि विश्लेषण प्रदान करता है, अर्थात कोई गलत नकारात्मक वापस नहीं किया जाता है। इसके अलावा, यह विश्लेषण की जाने वाली संपत्ति का प्रतिनिधित्व करने वाले अमूर्त डोमेन को ट्यून करके, और तेजी से अभिसरण प्राप्त करने के लिए व्यापक ऑपरेटरों को लागू करके, कुशलतापूर्वक विस्तार योग्य है।^[12]

Applications

आवेदन

राउटर, Ethernet स्विच, रूटिंग routing प्रोटोकॉल, सुरक्षा एप्लिकेशन और ऑपरेटिंग सिस्टम माइक्रोकर्नेल जैसे seL4 सहित हार्डवेयर और सॉफ्टवेयर के विभिन्न क्षेत्रों में औपचारिक तरीके लागू होते हैं। ऐसे कई उदाहरण हैं जिनमें इनका उपयोग DC में प्रयुक्त हार्डवेयर और सॉफ़्टवेयर की कार्यक्षमता को सत्यापित करने के लिए किया गया है^{[clarification needed]}. IBM ने AMD x86 संसाधक विकास प्रक्रिया में ACL2 , एक प्रमेय कहावत का उपयोग किया।^{[citation needed]} इंटेल अपने हार्डवेयर और फ़र्मवेयर को सत्यापित करने के लिए ऐसे तरीकों का उपयोग करता है (स्थायी सॉफ़्टवेयर को केवल पठनीय स्मृति में प्रोग्राम किया जाता है)^{[citation needed]}. डेनिश सूचना विज्ञान केंद्र ने 1980 के दशक में एडा (Ada) प्रोग्रामिंग भाषा के लिए एक कंपाइलर सिस्टम विकसित करने के लिए औपचारिक तरीकों का इस्तेमाल किया, जो एक लंबे समय तक चलने वाला व्यावसायिक उत्पाद बन गया।^[13]^[14] नासा की कई अन्य परियोजनाएं हैं जिनमें औपचारिक तरीकों को लागू किया जाता है, जैसे अगली पीढ़ी हवाई परिवहन प्रणाली^{[citation needed]}राष्ट्रीय हवाई क्षेत्र प्रणाली में मानवरहित विमान प्रणाली का एकीकरण,^[15] और एयरबोर्न कोऑर्डिनेटेड कॉन्फ्लिक्ट रेजोल्यूशन एंड डिटेक्शन (ACCoRD)।^[16] एटेलियर बी के साथ बी-विधि ,^[17] आल्सटॉम और सीमेंस द्वारा दुनिया भर में स्थापित विभिन्न उपमार्ग के लिए सुरक्षा स्वचालितता विकसित करने के लिए उपयोग किया जाता है, औरसामान्य मानदंड प्रमाणन औरएटीएमईएल और एसटीएमइक्रोइलेक्ट्रॉनिक्स द्वारा सिस्टम मॉडल के विकास के लिए भी उपयोग किया जाता है।

अधिकांश जाने-माने हार्डवेयर विक्रेताओं, जैसे आईबीएम, इंटेल और एएमडी द्वारा हार्डवेयर में औपचारिक सत्यापन अक्सर किया जाता है। हार्डवेयर के कई क्षेत्र हैं, जहां इंटेल ने उत्पादों के कामकाज को सत्यापित करने के लिए एफएम का उपयोग किया है, जैसे कैश-कोहेरेंट प्रोटोकॉल का पैरामीटरयुक्त सत्यापन,^[18] इंटेल कोर i7 संसाधक निष्पादन इंजन सत्यापन ^[19] (प्रमेय सिद्ध करने, द्विआधारी निर्णय आरेख,और प्रतीकात्मक मूल्यांकन का उपयोग करके), एचओएल प्रकाश प्रमेय प्रोवर का उपयोग करके इंटेल आईए -64 आर्किटेक्चर का इष्टतम उपयोग करके,^[20] और ताल का उपयोग करते हुए पीसीआई एक्सप्रेस प्रोटोकॉल और इंटेल अग्रिम प्रबंधन प्रौद्योगिकी के समर्थन के साथ उच्च-प्रदर्शन दोहरे पोर्ट गीगाबिट ईथरनेट नियंत्रक का सत्यापन।^[21] इसी तरह, आईबीएम ने पावर गेट्स के सत्यापन में औपचारिक तरीकों का इस्तेमाल किया है,^[22] रजिस्टर,^[23] और IBM Power7 माइक्रोसंसाधक के सत्यापन^[24] में औपचारिक तरीकों का इस्तेमाल किया है।

सॉफ्टवेयर विकास में

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

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

कार्यात्मक प्रोग्रामिंग में, संपत्ति-आधारित परीक्षण ने व्यक्तिगत कार्यों के अपेक्षित व्यवहार के गणितीय विनिर्देश और त्वरित परीक्षण (यदि संपूर्ण परीक्षण नहीं) की अनुमति दी है।

यदि ऑब्जेक्ट-ओरिएंटेड सिस्टम, औपचारिक रूप से सत्यापित नहीं किया गया है तो ऑब्जेक्ट बाधा भाषा (और विशेषज्ञता जैसे जावा मॉडलिंग भाषा) ने ऑब्जेक्ट-ओरिएंटेड सिस्टम को औपचारिक रूप से निर्दिष्ट करने की अनुमति दी है।

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

सॉफ्टवेयर विकास में औपचारिक तरीकों के लिए एक अन्य दृष्टिकोण तर्क के किसी रूप में एक विनिर्देश लिखना है - आमतौर परप्रथम-क्रम तर्क (एफओएल) की भिन्नता - और फिर तर्क को सीधे निष्पादित करना जैसे कि यह एक कार्यक्रम था। विवरण तर्क (DL), पर आधारित वेब ओन्टोलॉजी भाषा इसका एक उदाहरण है। साथ ही इसमें अंग्रेजी के कुछ संस्करण (या किसी अन्य प्राकृतिक भाषा) को तर्क से स्वचालित रूप से पता लगाने के साथ-साथ तर्क को सीधे निष्पादित करने पर भी काम होता है। उदाहरण हैं नियंत्रित अंग्रेजी का प्रयास,और इंटरनेट बिजनेस लॉजिक,जो शब्दावली या वाक्य-रचना को नियंत्रित करने की कोशिश नहीं करते हैं। सिस्टम की एक विशेषता जो द्विदिश अंग्रेजी-तर्क का पता लगाने के साथ-साथ तर्क के प्रत्यक्ष निष्पादन का समर्थन करती है, वह यह है कि उन्हें अपने परिणामों को अंग्रेजी में, व्यवसाय या वैज्ञानिक स्तर पर समझाने के लिए बनाया जा सकता है।^{[citation needed]}

औपचारिक तरीके और संकेतन

विभिन्न प्रकार के औपचारिक तरीके और संकेतन उपलब्ध हैं।

विशिष्टता भाषाएं

सार राज्य मशीनें (एएसएम)
ACL2 (ACL2)
अभिनेता मॉडल
मिश्र धातु भाषा
एएनएसआई/आईएसओ सी विशिष्टता भाषा (एसीएसएल)
स्वायत्त प्रणाली विशिष्टता भाषा (एएसएसएल)
बी-विधि
सीएडीपी
सामान्य बीजगणितीय विशिष्टता भाषा (CASL)
एस्टरेल
जावा मॉडलिंग लैंग्वेज (जेएमएल)
ज्ञान आधारित सॉफ्टवेयर सहायक (KBSA)
चमक प्रोग्रामिंग भाषा
तीखा
बिल्कुल सही डेवलपर
पेट्री डिश
प्रेडिक्टिव प्रोग्रामिंग
प्रक्रिया गणना
- अनुक्रमिक प्रक्रियाओं का संचार करना
- अस्थायी आदेश विशिष्टता की भाषा
- पाई-कैलकुलस|π-कैलकुलस
विनिर्देश भाषा बढ़ाएं
रेबेका मॉडलिंग भाषा
स्पार्क (प्रोग्रामिंग भाषा)
विनिर्देशन और विवरण भाषा
टीएलए+
यूनिवर्सल सिस्टम लैंग्वेज
वियना विकास विधि
- वीडीएम विनिर्देश भाषा |वीडीएम-एसएल
- वीडीएम++
जेड अंकन

मॉडल चेकर्स

ईएसबीएमसी^[25]
MALPAS सॉफ्टवेयर स्टेटिक एनालिसिस टूलसेट - एक औद्योगिक-शक्ति मॉडल चेकर जिसका उपयोग सुरक्षा-महत्वपूर्ण प्रणालियों के औपचारिक प्रमाण के लिए किया जाता है
पीएटी (मॉडल चेकर) - समवर्ती सिस्टम और सीएसपी एक्सटेंशन (जैसे, साझा चर, सरणियाँ, निष्पक्षता) के लिए एक मुफ्त मॉडल चेकर, सिम्युलेटर और शोधन परीक्षक
स्पिन मॉडल चेकर
उप्पल मॉडल चेकर

संगठन

यह भी देखें

सार व्याख्या
स्वचालित प्रमेय सिद्ध करना
अनुबंध द्वारा डिजाइन
:श्रेणी:औपचारिक तरीके लोग
औपचारिक विनिर्देश
औपचारिक सत्यापन
औपचारिक प्रणाली
मॉडल चेकिंग
सॉफ्टवेयर इंजीनियरिंग
विनिर्देश भाषा

संदर्भ

↑ Butler, R. W. (2001-08-06). "What is Formal Methods?". Retrieved 2006-11-16.
↑ Holloway, C. Michael. "Why Engineers Should Consider Formal Methods" (PDF). 16th Digital Avionics Systems Conference (27–30 October 1997). Archived from the original (PDF) on 16 November 2006. Retrieved 2006-11-16. {{cite journal}}: Cite journal requires |journal= (help)
↑ Monin, pp.3-4
↑ X2R-2, deliverable D5.1.
↑ Daniel Jackson and Jeannette Wing, "Lightweight Formal Methods", IEEE Computer, April 1996
↑ Vinu George and Rayford Vaughn, "Application of Lightweight Formal Methods in Requirement Engineering" Archived 2006-03-01 at the Wayback Machine, Crosstalk: The Journal of Defense Software Engineering, January 2003
↑ Daniel Jackson, "Alloy: A Lightweight Object Modelling Notation", ACM Transactions on Software Engineering and Methodology (TOSEM), Volume 11, Issue 2 (April 2002), pp. 256-290
↑ Richard Denney, Succeeding with Use Cases: Working Smart to Deliver Quality, Addison-Wesley Professional Publishing, 2005, ISBN 0-321-31643-6.
↑ Sten Agerholm and Peter G. Larsen, "A Lightweight Approach to Formal Methods" Archived 2006-03-09 at the Wayback Machine, In Proceedings of the International Workshop on Current Trends in Applied Formal Methods, Boppard, Germany, Springer-Verlag, October 1998
↑ Backus, J.W. (1959). "The Syntax and Semantics of the Proposed International Algebraic Language of Zürich ACM-GAMM Conference". Proceedings of the International Conference on Information Processing. UNESCO.
↑ Knuth, Donald E. (1964), Backus Normal Form vs Backus Naur Form. Communications of the ACM, 7(12):735–736.
↑ A. Cortesi and M. Zanioli, Widening and Narrowing Operators for Abstract Interpretation. Computer Languages, Systems and Structures. Volume 37(1), pp. 24–42, Elsevier, ISSN 1477-8424 (2011).
↑ Bjørner, Dines; Gram, Christian; Oest, Ole N.; Rystrøm, Leif (2011). "Dansk Datamatik Center". In Impagliazzo, John; Lundin, Per; Wangler, Benkt (eds.). History of Nordic Computing 3: IFIP Advances in Information and Communication Technology. Springer. pp. 350–359.
↑ Bjørner, Dines; Havelund, Klaus. "40 Years of Formal Methods: Some Obstacles and Some Possibilities?". FM 2014: Formal Methods: 19th International Symposium, Singapore, May 12–16, 2014. Proceedings (PDF). Springer. pp. 42–61.
↑ Gheorghe, A. V., & Ancel, E. (2008, November). Unmanned aerial systems integration to National Airspace System. In Infrastructure Systems and Services: Building Networks for a Brighter Future (INFRA), 2008 First International Conference on (pp. 1-5). IEEE.
↑ Airborne Coordinated Conflict Resolution and Detection, http://shemesh.larc.nasa.gov/people/cam/ACCoRD/
↑ "Atelier B". www.atelierb.eu (in English).
↑ C. T. Chou, P. K. Mannava, S. Park, “A simple method for parameterized verification of cache coherence protocols”, Formal Methods in Computer-Aided Design, pp. 382–398, 2004.
↑ Formal Verification in Intel® Core™ i7 Processor Execution Engine Validation, http://cps-vo.org/node/1371, accessed at Sep. 13, 2013.
↑ J. Grundy, “Verified optimizations for the Intel IA-64 architecture”, In Theorem Proving in Higher Order Logics, Springer Berlin Heidelberg, 2004, pp. 215–232.
↑ E. Seligman, I. Yarom, “Best known methods for using Cadence Conformal LEC”, at Intel.
↑ C. Eisner, A. Nahir, K. Yorav, “Functional verification of power gated designs by compositional reasoning”, Computer Aided Verification, Springer Berlin Heidelberg, pp. 433–445.
↑ P. C. Attie, H. Chockler, “Automatic verification of fault-tolerant register emulations”, Electronic Notes in Theoretical Computer Science, vol. 149, no. 1, pp. 49–60.
↑ K. D. Schubert, W. Roesner, J. M. Ludden, J. Jackson, J. Buchert, V. Paruthi, B. Brock, “Functional verification of the IBM POWER7 microprocessor and POWER7 multiprocessor systems”, IBM Journal of Research and Development, vol. 55, no 3.
↑ "ESBMC". esbmc.org.

इस पृष्ठ में अनुपलब्ध आंतरिक कड़ियों की सूची

विशिष्ट एकीकृत परिपथ आवेदन
डिजिटल डाटा
आंकड़े
के माध्यम से (इलेक्ट्रॉनिक्स)
संवहन दस्तावेज़ स्वरूप
विनिर्माण क्षमता के लिए डिजाइन (आईसी)
सिलिकॉन सत्यापन पोस्ट करें
मास्क डेटा तैयारी
असफलता विश्लेषण
रजिस्टर ट्रांसफर लेवल
सी (प्रोग्रामिंग भाषा)
यात्रा
मांग
उत्पाद आवश्यकता दस्तावेज़
बाज़ार अवसर
जीवन का अंत (उत्पाद)
निर्देश समुच्चय
तर्क अनुकरण
सिग्नल की समग्रता
डिजाइन नियम की जाँच
टाइमिंग क्लोजर
औपचारिक तुल्यता जाँच
सामान्य केन्द्रक
ऑप एंप
मेंटर ग्राफिक्स
एकीकृत परिपथों और प्रणालियों के कंप्यूटर सहायता प्राप्त डिजाइन पर आईईईई लेनदेन
असफलता विश्लेषण
एन पी-सम्पूर्ण
परीक्षण वेक्टर
controllability
observability
प्रशंसक एल्गोरिदम
कूट-यादृच्छिक
पंक्ति का पिछला अंत
बांड विशेषता
दोहरी इन-लाइन पैकेज
मरो (एकीकृत सर्किट)
निर्माण (अर्धचालक)
विद्युतचुंबकीय व्यवधान
epoxy
भली भांति बंद सील
फ्लैटपैक (इलेक्ट्रॉनिक्स)
पतली छोटी रूपरेखा पैकेज
गोंद
मेटलाइजिंग
अनावर्ती अभियांत्रिकी
बाजार के लिए समय
तार का जोड़
नमी
विद्युतीय
स्थानीय कर से मुक्ति
साफ-सुथरे कमरे
अवरोधित हो जाना
HIRF
एकीकृत परिपथ
रूटिंग (इलेक्ट्रॉनिक डिजाइन ऑटोमेशन)
प्रक्रिया के कोने
मानक सेल
आईसी बिजली की आपूर्ति पिन
घड़ी की आवृत्ति
सिग्नल की समग्रता
उत्तम नस्ल
रजिस्टर ट्रांसफर लेवल
मूल्य संवर्धित
पुस्तकालय (कंप्यूटर विज्ञान)
मॉडल आधारित डिजाइन
स्वत: नियंत्रण
राज्य मशीनें
सोर्स कोड
स्वचालित कोड पीढ़ी
शून्य से विभाजन
आवश्यकताओं का पता लगाने योग्यता
मॉडल जांच
औपचारिक तरीके
मॉडल केंद्र
वेब आधारित अनुकरण
Xcos
साइलैब
पूर्णांक
मैक ओएस
प्रयोक्ता इंटरफ़ेस
समारोह (गणित)
फोरट्रान
स्थिर (कंप्यूटर विज्ञान)
खिसकाना
जादू वर्ग
लैम्ब्डा कैलकुलस
मेक्स फ़ाइल
मेथेमेटिका
तुम क्या सहन करते हो
संख्यात्मक-विश्लेषण सॉफ्टवेयर की तुलना
आईईईई मानक
एक्सेलेरा
जावा (प्रोग्रामिंग भाषा)
पैक्ड सरणी
कड़ा मुकाबला
struct
टाइपडीफ
कुंडी (इलेक्ट्रॉनिक)
रन टाइम (कार्यक्रम जीवनचक्र चरण)
एकल विरासत
टेम्पलेट विशेषज्ञता
जानकारी छिपाना
ऑपरेटर नया
यादृच्छिक परीक्षण
सामग्री निहितार्थ (अनुमान का नियम)
पूर्ववृत्त (तर्क)
फलस्वरूप
सिमुलेशन
स्वचालित प्रमेय सिद्ध करना
कार्तीय गुणन
परीक्षण के अंतर्गत उपकरण
डिजाइन अंतरिक्ष सत्यापन
टेस्ट कवरेज
उदाहरण (कंप्यूटर विज्ञान)
तुल्यकालन (कंप्यूटर विज्ञान)
सशक्त टाइपिंग
पाश के लिए
बहाव को काबू करें
लगातार (कंप्यूटर प्रोग्रामिंग)
भाषा अंतरसंचालनीयता
सी-परिवार प्रोग्रामिंग भाषाओं की सूची
प्रक्रमण करने से पहले के निर्देश
मूल फाइल
लिंट (सॉफ्टवेयर)
एकीकृत सर्किट डिजाइन
एकीकृत सर्किट लेआउट
एकीकृत परिपथ
पूरा रिवाज
इन्सुलेटर पर सिलिकॉन
मुखौटा डेटा तैयारी
उच्च स्तरीय संश्लेषण
असतत घटना सिमुलेशन
आईडिया1
उच्च स्तरीय प्रोग्रामिंग भाषा
संगणक वैज्ञानिक
वितरित अभिकलन
व्युत्पन्न वर्ग
सीएलयू (प्रोग्रामिंग भाषा)
अदा (प्रोग्रामिंग भाषा)
कक्षा (कंप्यूटर प्रोग्रामिंग)
कास्ट (कंप्यूटर विज्ञान)
एक्सेप्शन हेंडलिंग
सभा की भाषा
अवधारणाएं (सी ++)
सी ++ मानक पुस्तकालय
एब्स्ट्रैक्शन (कंप्यूटर साइंस)
कक्षा (कंप्यूटर विज्ञान)
संकलन समय
सहयोगी सरणी
सुविधा (सॉफ्टवेयर डिजाइन)
अनवरत वृद्धि # अनियंत्रित विस्तार
विशिष्ट एकीकृत परिपथ आवेदन
अर्धचालक निर्माण
एक चिप पर सिस्टम
नि: शुल्क
अनुक्रमिक तर्क
स्थान और मार्ग
रूटिंग (ईडीए)
सेमीकंडक्टर
आर्किटेक्ट
फ्लोरेंस कैथेड्रल
वास्तु सिद्धांत
समसामयिक आर्किटेक्चर
गोथिक वास्तुशिल्प
फार्म समारोह के बाद
मंजिल की योजना
सुनहरा अनुपात
वास्तुकला डिजाइन मूल्य
पुनर्निर्माणवाद
क्लासिकल एंटिक्विटी
कैथेड्रल
सौंदर्यशास्र
अभिव्यंजनावादी वास्तुकला
वास्तु घटना विज्ञान
हरा भवन
हरित बुनियादी ढाँचा
संकल्पनात्मक निदर्श
व्‍यवहार
वास्तुकला प्रौद्योगिकी
कटलरी
डिजाइन के तरीके
संकल्पनात्मक निदर्श
झरना मॉडल
शोध करना
उत्पाद डिजाइन विनिर्देश
संक्षिप्त आकार
उत्पाद का परीक्षण करना
समस्या को सुलझाना
दस्तावेज़
साइट पर
आशुरचना
चुस्त सॉफ्टवेयर विकास
उपयोगकर्ता केंद्रित डिजाइन
ग्राफक कला
एप्लाइड आर्ट्स
मुहावरा
चिन्ह, प्रतीक
जानबूझकर परिभाषा
अंक शास्त्र
सूक्तियों
आवश्यक और पर्याप्त शर्तें
लिंग-अंतर परिभाषा
त्रिकोण
चतुष्कोष
पदार्थवाद
संभव दुनिया
कठोर अभिकर्ता
संचालनगत परिभाषा
समनाम
निराकरण
संकेत (सेमियोटिक्स)
सेमे (शब्दार्थ)
शब्द भावना
अर्थ क्षेत्र
अर्थ (भाषाविज्ञान)
निओलगिज़्म
अपरिष्कृत किस्म
परिभाषा के अनुसार विस्तार
आत्म संदर्भ
चिकित्सा सहमति
चिकित्सा वर्गीकरण
शाब्दिक परिभाषा
मतवाद
प्राणी
दार्शनिक जांच
व्यक्तित्व का सिद्धांत
विवरण का सिद्धांत
शाऊल क्रिप्के
अनिश्चितता (दर्शनशास्त्र)
अर्थ विज्ञान
जानकारी
सरल भाषा
भाषा: हिन्दी
बातचीत का माध्यम
सूचना प्रक्रम
गुप्तता
लिख रहे हैं
आधार - सामग्री संकोचन
हाव-भाव
कुल कार्य
कड़ी
कोड वर्ड
कम घनत्व समता-जांच कोड
उच्चारण क्षमता
चरित्र (कंप्यूटिंग)
एचटीटीपी हेडर
जेनेटिक कोड
जीवविज्ञान
अवरोध
पत्रक संगीत
क्रिप्टोग्राफी का इतिहास
पाठ के प्रस्तुतिकरण के लिए प्रयुक्त भाषा
टेक्स्ट एन्कोडिंग पहल
SECAM
शब्दार्थ एन्कोडिंग
मेमोरी एन्कोडिंग
लेखन प्रणाली
सांकेतिकता
कोड (सेमियोटिक्स)
असिमिक लेखन
जाँचने का तरीका
निहाई
बरबाद करना
प्रथम लेख निरीक्षण
प्राथमिक धारा
फाइल का प्रारूप
फ़ाइल साझा करना
सर्वाधिकार उल्लंघन
संशोधित असतत कोसाइन परिवर्तन
अंतरराष्ट्रीय मानकीकरण संगठन
इंटरनेशनल इलेक्ट्रोटेक्नीकल कमीशन
बुंदाडा इटाकुरा
असतत कोसाइन परिवर्तन
फिल्टर (सॉफ्टवेयर)
धोखाधड़ी
एमपीईजी-1 ऑडियो परत II
झूठा
नमूनाकरण दर
संदर्भ कार्यान्वयन (कंप्यूटिंग)
सोल
धुन (ऑनलाइन संगीत सेवा)
जॉइन्ट स्टीरियो
त्रुटि की जांच कर रहा है
पूर्व बनाया
संपीड़न विरूपण साक्ष्य
लाल किताब (ऑडियो सीडी मानक)
आईएफए शो
कार्य (ऑडियो प्रारूप)
सेब दोषरहित
एमपीईजी -4 भाग 14
बयान (कंप्यूटर विज्ञान)
सॉफ़्टवेयर परीक्षण
एसीएम का संचार
सुरक्षा महत्वपूर्ण
परिमित अवस्था मशीन
रुकने की समस्या
ताल डिजाइन सिस्टम
एफपीजीए प्रोटोटाइप
कदम स्तर
एम्यूलेटर
उन्नत लघु उपकरण
सेंट्रल प्रोसेसिंग यूनिट
स्पर्धारोधी कानून
शुरुआती सार्वजानिक प्रस्ताव
क्रेग बैरेट (व्यापारी)
एंटीट्रस्ट
एआईएम गठबंधन
किफायती इंटरनेट के लिए गठबंधन
सेब सिलिकॉन
EPROM
विद्युत ऊर्जा की खपत
एम्बर झील (सूक्ष्म वास्तुकला)
Apple वर्ल्डवाइड डेवलपर्स कॉन्फ्रेंस
स्वतंत्र रूप से पुनर्वितरण योग्य सॉफ्टवेयर
प्रचार अभियान
प्रतिस्पर्धी विरोधी प्रथाएं
एथिलबेन्जीन
संघर्ष संसाधन
कन्फ्लिक्ट खनिज
आयु भेदभाव
बम्पलेस बिल्ड-अप परत
उत्पाद वापसी
प्रधान चौगुनी
प्राइम ट्रिपलेट
जुड़वां प्रधान
प्रतीकात्मक प्रक्षेपवक्र मूल्यांकन
कदम स्तर
पुस्तकालय (कम्प्यूटिंग)
औपचारिक विशिष्टता
सिस्टम टाइप करें
कंप्यूटर विज्ञान में तर्क
शर्त लगाना
कार्यक्रम परिशोधन
स्वचालित प्रमेय कहावत
जेड अंकन
उदाहरण
अनिश्चितता
ओरेकल मशीन
एडीए प्रोग्रामिंग भाषा
वस्तु बाधा भाषा
परिमित अवस्था मशीन
आभासी परिमित राज्य मशीन
औद्योगिक सॉफ्टवेयर इंजीनियरिंग के लिए कठोर दृष्टिकोण
विशिष्टता और विवरण भाषा
RAISE विनिर्देश भाषा
विशिष्टता भाषा

अग्रिम पठन

Jonathan P. Bowen and Michael G. Hinchey, Formal Methods. In Allen B. Tucker, Jr. (ed.), Computer Science Handbook, 2nd edition, Section XI, Software Engineering, Chapter 106, pages 106-1 – 106-25, Chapman & Hall / CRC Press, Association for Computing Machinery, 2004.
Hubert Garavel (editor) and Susanne Graf. Formal Methods for Safe and Secure Computer Systems. Bundesamt für Sicherheit in der Informationstechnik, BSI study 875, Bonn, Germany, December 2013.
Garavel, Hubert; ter Beek, Maurice H.; van de Pol, Jaco (29 August 2020). "The 2020 Expert Survey on Formal Methods". Formal Methods for Industrial Critical Systems: 25 International Conference, FMICS 2020 (PDF). Lecture Notes in Computer Science (LNCS). Vol. 12327. Springer. pp. 3–69. doi:10.1007/978-3-030-58298-2_1. ISBN 978-3-030-58297-5. S2CID 221381022.* Michael G. Hinchey, Jonathan P. Bowen, and Emil Vassev, Formal Methods. In Philip A. Laplante (ed.), Encyclopedia of Software Engineering, Taylor & Francis, 2010, pages 308–320.
Marieke Huisman, Dilian Gurov, and Alexander Malkis, Formal Methods: From Academia to Industrial Practice – A Travel Guide, arXiv:2002.07279, 2020.
Gleirscher, Mario; Marmsoler, Diego (9 September 2020). "Formal methods in dependable systems engineering: a survey of professionals from Europe and North America". Empirical Software Engineering. Springer Nature. 25 (6): 4473–4546. doi:10.1007/s10664-020-09836-5.
Jean François Monin and Michael G. Hinchey, Understanding formal methods, Springer, 2003, ISBN 1-85233-247-6.

बाहरी संबंध

Archival material

Formal method keyword on Microsoft Academic Search via Archive.org
Evidence on Formal Methods uses and impact on Industry supported by the DEPLOY project (EU FP7) in Archive.org

[butler-1] Butler, R. W. (2001-08-06). "What is Formal Methods?". Retrieved 2006-11-16.

[2] Holloway, C. Michael. "Why Engineers Should Consider Formal Methods" (PDF). 16th Digital Avionics Systems Conference (27–30 October 1997). Archived from the original (PDF) on 16 November 2006. Retrieved 2006-11-16. {{cite journal}}: Cite journal requires |journal= (help)

[3] Monin, pp.3-4

[4] X2R-2, deliverable D5.1.

[5] Daniel Jackson and Jeannette Wing, "Lightweight Formal Methods", IEEE Computer, April 1996

[6] Vinu George and Rayford Vaughn, "Application of Lightweight Formal Methods in Requirement Engineering" Archived 2006-03-01 at the Wayback Machine, Crosstalk: The Journal of Defense Software Engineering, January 2003

[7] Daniel Jackson, "Alloy: A Lightweight Object Modelling Notation", ACM Transactions on Software Engineering and Methodology (TOSEM), Volume 11, Issue 2 (April 2002), pp. 256-290

[8] Richard Denney, Succeeding with Use Cases: Working Smart to Deliver Quality, Addison-Wesley Professional Publishing, 2005, ISBN 0-321-31643-6.

[9] Sten Agerholm and Peter G. Larsen, "A Lightweight Approach to Formal Methods" Archived 2006-03-09 at the Wayback Machine, In Proceedings of the International Workshop on Current Trends in Applied Formal Methods, Boppard, Germany, Springer-Verlag, October 1998

[10] Backus, J.W. (1959). "The Syntax and Semantics of the Proposed International Algebraic Language of Zürich ACM-GAMM Conference". Proceedings of the International Conference on Information Processing. UNESCO.

[11] Knuth, Donald E. (1964), Backus Normal Form vs Backus Naur Form. Communications of the ACM, 7(12):735–736.

[12] A. Cortesi and M. Zanioli, Widening and Narrowing Operators for Abstract Interpretation. Computer Languages, Systems and Structures. Volume 37(1), pp. 24–42, Elsevier, ISSN 1477-8424 (2011).

[13] Bjørner, Dines; Gram, Christian; Oest, Ole N.; Rystrøm, Leif (2011). "Dansk Datamatik Center". In Impagliazzo, John; Lundin, Per; Wangler, Benkt (eds.). History of Nordic Computing 3: IFIP Advances in Information and Communication Technology. Springer. pp. 350–359.

[14] Bjørner, Dines; Havelund, Klaus. "40 Years of Formal Methods: Some Obstacles and Some Possibilities?". FM 2014: Formal Methods: 19th International Symposium, Singapore, May 12–16, 2014. Proceedings (PDF). Springer. pp. 42–61.

[15] Gheorghe, A. V., & Ancel, E. (2008, November). Unmanned aerial systems integration to National Airspace System. In Infrastructure Systems and Services: Building Networks for a Brighter Future (INFRA), 2008 First International Conference on (pp. 1-5). IEEE.

[16] Airborne Coordinated Conflict Resolution and Detection, http://shemesh.larc.nasa.gov/people/cam/ACCoRD/

[17] "Atelier B". www.atelierb.eu (in English).

[18] C. T. Chou, P. K. Mannava, S. Park, “A simple method for parameterized verification of cache coherence protocols”, Formal Methods in Computer-Aided Design, pp. 382–398, 2004.

[19] Formal Verification in Intel® Core™ i7 Processor Execution Engine Validation, http://cps-vo.org/node/1371, accessed at Sep. 13, 2013.

[20] J. Grundy, “Verified optimizations for the Intel IA-64 architecture”, In Theorem Proving in Higher Order Logics, Springer Berlin Heidelberg, 2004, pp. 215–232.

[21] E. Seligman, I. Yarom, “Best known methods for using Cadence Conformal LEC”, at Intel.

[22] C. Eisner, A. Nahir, K. Yorav, “Functional verification of power gated designs by compositional reasoning”, Computer Aided Verification, Springer Berlin Heidelberg, pp. 433–445.

[23] P. C. Attie, H. Chockler, “Automatic verification of fault-tolerant register emulations”, Electronic Notes in Theoretical Computer Science, vol. 149, no. 1, pp. 49–60.

[24] K. D. Schubert, W. Roesner, J. M. Ludden, J. Jackson, J. Buchert, V. Paruthi, B. Brock, “Functional verification of the IBM POWER7 microprocessor and POWER7 multiprocessor systems”, IBM Journal of Research and Development, vol. 55, no 3.

[25] "ESBMC". esbmc.org.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]

[19]

[20]

[21]

[22]

[23]

[24]

[25]

@@ Line 18: / Line 18: @@
 स्तर 1: [[ औपचारिक विकास |औपचारिक विकास]] और औपचारिक सत्यापन का उपयोग किसी कार्यक्रम को अधिक औपचारिक तरीके से तैयार करने के लिए किया जा सकता है। उदाहरण के लिए, किसी कार्यक्रम के औपचारिक विनिर्देश से गुणों या कार्यक्रम के शोधन के प्रमाण किए जा सकते हैं। यह[[ सुरक्षा | सुरक्षा]] से जुड़े उच्च-अखंडता प्रणालियों में सबसे उपयुक्त हो सकता है।
-स्तर 2:  प्रमेय प्रोवर्स का उपयोग पूरी तरह से औपचारिक मशीन-चेक किए गए प्रमाणों को करने के लिए किया जा सकता है। यदि गलतियों की लागत बहुत अधिक है तो उपकरणों में सुधार और घटती लागत के बावजूद, यह बहुत महंगा हो सकता है जो की केवल व्यावहारिक रूप से सार्थक है (उदाहरण के लिए, ऑपरेटिंग सिस्टम या माइक्रोप्रोसेसर डिजाइन के महत्वपूर्ण भागों में)।
+स्तर 2:  प्रमेय प्रोवर्स का उपयोग पूरी तरह से औपचारिक मशीन-चेक किए गए प्रमाणों को करने के लिए किया जा सकता है। यदि गलतियों की लागत बहुत अधिक है तो उपकरणों में सुधार और घटती लागत के बावजूद, यह बहुत महंगा हो सकता है जो की केवल व्यावहारिक रूप से सार्थक है (उदाहरण के लिए, ऑपरेटिंग सिस्टम या माइक्रोसंसाधक डिजाइन के महत्वपूर्ण भागों में)।
 इसके बारे में अधिक जानकारी नीचे दी गई है।
@@ Line 82: / Line 82: @@
 == आवेदन ==
-राउटर, ईथरनेट स्विच, रूटिंग प्रोटोकॉल, सुरक्षा एप्लिकेशन और ऑपरेटिंग सिस्टम माइक्रोकर्नेल जैसे [[ seL4 ]] सहित हार्डवेयर और सॉफ्टवेयर के विभिन्न क्षेत्रों में औपचारिक तरीके लागू होते हैं। ऐसे कई उदाहरण हैं जिनमें इनका उपयोग DC में प्रयुक्त हार्डवेयर और सॉफ़्टवेयर की कार्यक्षमता को सत्यापित करने के लिए किया गया है{{clarify|date=September 2015}}. [[ IBM ]] ने [[ AMD ]] x86 प्रोसेसर विकास प्रक्रिया में [[ ACL2 ]], एक प्रमेय कहावत का उपयोग किया।{{citation needed|date=September 2015}} इंटेल अपने हार्डवेयर और फ़र्मवेयर को सत्यापित करने के लिए ऐसे तरीकों का उपयोग करता है (स्थायी सॉफ़्टवेयर को केवल-पढ़ने के लिए मेमोरी में प्रोग्राम किया जाता है){{citation needed|date=September 2015}}. [[ डेनिश सूचना विज्ञान केंद्र ]] ने 1980 के दशक में एडा प्रोग्रामिंग भाषा के लिए एक कंपाइलर सिस्टम विकसित करने के लिए औपचारिक तरीकों का इस्तेमाल किया, जो एक लंबे समय तक चलने वाला व्यावसायिक उत्पाद बन गया।<ref>{{cite book | first1=Dines | last1=Bjørner | first2=Christian | last2=Gram | first3=Ole N. | last3=Oest | first4=Leif | last4=Rystrøm | chapter=Dansk Datamatik Center | editor-first= John | editor-last=Impagliazzo | editor2-first=Per | editor2-last=Lundin | editor3-first=Benkt | editor3-last=Wangler | title=History of Nordic Computing 3: IFIP Advances in Information and Communication Technology | publisher=Springer | year= 2011 | pages= 350–359 }}</ref><ref>{{cite conference | contribution=40 Years of Formal Methods: Some Obstacles and Some Possibilities? | first1=Dines | last1=Bjørner | first2=Klaus | last2=Havelund | title=FM 2014: Formal Methods: 19th International Symposium, Singapore, May 12–16, 2014. Proceedings | publisher=Springer | pages=42–61 |url=http://www.imm.dtu.dk/~dibj/2014/tokyo/tokyo-s.pdf}}</ref>
+राउटर, Ethernet स्विच, रूटिंग routing प्रोटोकॉल, सुरक्षा एप्लिकेशन और ऑपरेटिंग सिस्टम माइक्रोकर्नेल जैसे [[ seL4 ]] सहित हार्डवेयर और सॉफ्टवेयर के विभिन्न क्षेत्रों में औपचारिक तरीके लागू होते हैं। ऐसे कई उदाहरण हैं जिनमें इनका उपयोग DC में प्रयुक्त हार्डवेयर और सॉफ़्टवेयर की कार्यक्षमता को सत्यापित करने के लिए किया गया है{{clarify|date=September 2015}}. [[ IBM ]] ने [[ AMD ]] x86 संसाधक विकास प्रक्रिया में [[ ACL2 ]], एक प्रमेय कहावत का उपयोग किया।{{citation needed|date=September 2015}} इंटेल अपने हार्डवेयर और फ़र्मवेयर को सत्यापित करने के लिए ऐसे तरीकों का उपयोग करता है (स्थायी सॉफ़्टवेयर को केवल पठनीय स्मृति में प्रोग्राम किया जाता है){{citation needed|date=September 2015}}. [[ डेनिश सूचना विज्ञान केंद्र ]] ने 1980 के दशक में एडा (Ada) प्रोग्रामिंग भाषा के लिए एक कंपाइलर सिस्टम विकसित करने के लिए औपचारिक तरीकों का इस्तेमाल किया, जो एक लंबे समय तक चलने वाला व्यावसायिक उत्पाद बन गया।<ref>{{cite book | first1=Dines | last1=Bjørner | first2=Christian | last2=Gram | first3=Ole N. | last3=Oest | first4=Leif | last4=Rystrøm | chapter=Dansk Datamatik Center | editor-first= John | editor-last=Impagliazzo | editor2-first=Per | editor2-last=Lundin | editor3-first=Benkt | editor3-last=Wangler | title=History of Nordic Computing 3: IFIP Advances in Information and Communication Technology | publisher=Springer | year= 2011 | pages= 350–359 }}</ref><ref>{{cite conference | contribution=40 Years of Formal Methods: Some Obstacles and Some Possibilities? | first1=Dines | last1=Bjørner | first2=Klaus | last2=Havelund | title=FM 2014: Formal Methods: 19th International Symposium, Singapore, May 12–16, 2014. Proceedings | publisher=Springer | pages=42–61 |url=http://www.imm.dtu.dk/~dibj/2014/tokyo/tokyo-s.pdf}}</ref>
-[[ नासा ]] की कई अन्य परियोजनाएं हैं जिनमें औपचारिक तरीकों को लागू किया जाता है, जैसे [[ अगली पीढ़ी हवाई परिवहन प्रणाली ]]{{citation needed|date=September 2015}}राष्ट्रीय हवाई क्षेत्र प्रणाली में मानवरहित विमान प्रणाली का एकीकरण,<ref>Gheorghe, A. V., & Ancel, E. (2008, November). Unmanned aerial systems integration to National Airspace System. In Infrastructure Systems and Services: Building Networks for a Brighter Future (INFRA), 2008 First International Conference on (pp. 1-5). IEEE.</ref> और एयरबोर्न कोऑर्डिनेटेड कॉन्फ्लिक्ट रेजोल्यूशन एंड डिटेक्शन (ACCoRD)।<ref>Airborne Coordinated Conflict Resolution and Detection, http://shemesh.larc.nasa.gov/people/cam/ACCoRD/</ref>
+[[ नासा ]] की कई अन्य परियोजनाएं हैं जिनमें औपचारिक तरीकों को लागू किया जाता है, जैसे [[ अगली पीढ़ी हवाई परिवहन प्रणाली |अगली पीढ़ी हवाई परिवहन प्रणाली]] {{citation needed|date=September 2015}}राष्ट्रीय हवाई क्षेत्र प्रणाली में मानवरहित विमान प्रणाली का एकीकरण,<ref>Gheorghe, A. V., & Ancel, E. (2008, November). Unmanned aerial systems integration to National Airspace System. In Infrastructure Systems and Services: Building Networks for a Brighter Future (INFRA), 2008 First International Conference on (pp. 1-5). IEEE.</ref> और एयरबोर्न कोऑर्डिनेटेड कॉन्फ्लिक्ट रेजोल्यूशन एंड डिटेक्शन (ACCoRD)।<ref>Airborne Coordinated Conflict Resolution and Detection, http://shemesh.larc.nasa.gov/people/cam/ACCoRD/</ref>
-[[ एटेलियर बी ]] के साथ [[ बी-विधि ]],<ref>{{cite web| url=http://www.atelierb.eu/en/ | title=Atelier B | website=www.atelierb.eu | lang=en }}</ref> [[ आल्सटॉम ]] और [[ सीमेंस ]] द्वारा दुनिया भर में स्थापित विभिन्न सबवे के लिए सुरक्षा स्वचालितता विकसित करने के लिए उपयोग किया जाता है, और [[ सामान्य मानदंड ]] प्रमाणन और [[ एटीएमईएल ]] और [[ एसटीएमइक्रोइलेक्ट्रॉनिक्स ]] द्वारा सिस्टम मॉडल के विकास के लिए भी उपयोग किया जाता है।
+[[ एटेलियर बी ]] के साथ [[ बी-विधि ]],<ref>{{cite web| url=http://www.atelierb.eu/en/ | title=Atelier B | website=www.atelierb.eu | lang=en }}</ref> [[ आल्सटॉम ]] और [[ सीमेंस ]] द्वारा दुनिया भर में स्थापित विभिन्न उपमार्ग के लिए सुरक्षा स्वचालितता विकसित करने के लिए उपयोग किया जाता है, और[[ सामान्य मानदंड |सामान्य मानदंड]] प्रमाणन और[[ एटीएमईएल ]]और [[ एसटीएमइक्रोइलेक्ट्रॉनिक्स |एसटीएमइक्रोइलेक्ट्रॉनिक्स]] द्वारा सिस्टम मॉडल के विकास के लिए भी उपयोग किया जाता है।
-अधिकांश जाने-माने हार्डवेयर विक्रेताओं, जैसे आईबीएम, [[ इंटेल ]] और एएमडी द्वारा हार्डवेयर में औपचारिक सत्यापन का उपयोग अक्सर किया जाता है। हार्डवेयर के कई क्षेत्र हैं, जहां इंटेल ने उत्पादों के कामकाज को सत्यापित करने के लिए एफएम का उपयोग किया है, जैसे कैश-कोहेरेंट प्रोटोकॉल का पैरामीटरयुक्त सत्यापन,<ref>C. T. Chou, P. K. Mannava, S. Park, “[https://www.student.cs.uwaterloo.ca/~cs745/paper-pres/simparam.pdf A simple method for parameterized verification of cache coherence protocols]”, Formal Methods in Computer-Aided Design, pp. 382–398, 2004.</ref> इंटेल कोर i7 प्रोसेसर निष्पादन इंजन सत्यापन <ref>Formal Verification in Intel® Core™ i7 Processor Execution Engine Validation, http://cps-vo.org/node/1371, accessed at Sep. 13, 2013.</ref> (प्रमेय सिद्ध करने, [[ द्विआधारी निर्णय आरेख ]], और प्रतीकात्मक मूल्यांकन का उपयोग करके), एचओएल प्रकाश प्रमेय प्रोवर का उपयोग करके इंटेल आईए -64 आर्किटेक्चर के लिए अनुकूलन,<ref>J. Grundy, “Verified optimizations for the Intel IA-64 architecture”, In Theorem Proving in Higher Order Logics, Springer Berlin Heidelberg, 2004, pp. 215–232.</ref> और ताल का उपयोग करते हुए पीसीआई एक्सप्रेस प्रोटोकॉल और इंटेल एडवांस मैनेजमेंट टेक्नोलॉजी के समर्थन के साथ उच्च-प्रदर्शन दोहरे पोर्ट गीगाबिट ईथरनेट नियंत्रक का सत्यापन।<ref>E. Seligman, I. Yarom, “[http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.108.2381&rep=rep1&type=pdf Best known methods for using Cadence Conformal LEC]”, at Intel.</ref> इसी तरह, आईबीएम ने पावर गेट्स के सत्यापन में औपचारिक तरीकों का इस्तेमाल किया है,<ref>C. Eisner, A. Nahir, K. Yorav, “[ftp://nozdr.ru/biblio/kolxo3/Cs/CsLn/Computer%20Aided%20Verification,%2020%20conf.,%20CAV%202008(LNCS5123,%20Springer,%202008)(ISBN%209783540705437)(573s)_CsLn_.pdf#page=449 Functional verification of power gated designs by compositional reasoning]”, Computer Aided Verification, Springer Berlin Heidelberg, pp. 433–445.</ref> रजिस्टर,<ref>P. C. Attie, H. Chockler, “[https://core.ac.uk/download/pdf/82434920.pdf Automatic verification of fault-tolerant register emulations]”, Electronic Notes in Theoretical Computer Science, vol. 149, no. 1, pp. 49–60.</ref> और IBM Power7 माइक्रोप्रोसेसर का कार्यात्मक सत्यापन।<ref>K. D. Schubert, W. Roesner, J. M. Ludden, J. Jackson, J. Buchert, V. Paruthi, B. Brock, “[https://ieeexplore.ieee.org/abstract/document/5756329/ Functional verification of the IBM POWER7 microprocessor and POWER7 multiprocessor systems]”, IBM Journal of Research and Development, vol. 55, no 3.</ref>
+अधिकांश जाने-माने हार्डवेयर विक्रेताओं, जैसे आईबीएम,[[ इंटेल | इंटेल]] और एएमडी द्वारा हार्डवेयर में औपचारिक सत्यापन अक्सर किया जाता है। हार्डवेयर के कई क्षेत्र हैं, जहां इंटेल ने उत्पादों के कामकाज को सत्यापित करने के लिए एफएम का उपयोग किया है, जैसे कैश-कोहेरेंट प्रोटोकॉल का पैरामीटरयुक्त सत्यापन,<ref>C. T. Chou, P. K. Mannava, S. Park, “[https://www.student.cs.uwaterloo.ca/~cs745/paper-pres/simparam.pdf A simple method for parameterized verification of cache coherence protocols]”, Formal Methods in Computer-Aided Design, pp. 382–398, 2004.</ref> इंटेल कोर i7 संसाधक निष्पादन इंजन सत्यापन <ref>Formal Verification in Intel® Core™ i7 Processor Execution Engine Validation, http://cps-vo.org/node/1371, accessed at Sep. 13, 2013.</ref> (प्रमेय सिद्ध करने,[[ द्विआधारी निर्णय आरेख | द्विआधारी निर्णय आरेख]],और प्रतीकात्मक मूल्यांकन का उपयोग करके), एचओएल प्रकाश प्रमेय प्रोवर का उपयोग करके इंटेल आईए -64 आर्किटेक्चर का इष्टतम उपयोग करके,<ref>J. Grundy, “Verified optimizations for the Intel IA-64 architecture”, In Theorem Proving in Higher Order Logics, Springer Berlin Heidelberg, 2004, pp. 215–232.</ref> और ताल का उपयोग करते हुए पीसीआई एक्सप्रेस प्रोटोकॉल और इंटेल अग्रिम प्रबंधन प्रौद्योगिकी के समर्थन के साथ उच्च-प्रदर्शन दोहरे पोर्ट गीगाबिट ईथरनेट नियंत्रक का सत्यापन।<ref>E. Seligman, I. Yarom, “[http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.108.2381&rep=rep1&type=pdf Best known methods for using Cadence Conformal LEC]”, at Intel.</ref> इसी तरह, आईबीएम ने पावर गेट्स के सत्यापन में औपचारिक तरीकों का इस्तेमाल किया है,<ref>C. Eisner, A. Nahir, K. Yorav, “[ftp://nozdr.ru/biblio/kolxo3/Cs/CsLn/Computer%20Aided%20Verification,%2020%20conf.,%20CAV%202008(LNCS5123,%20Springer,%202008)(ISBN%209783540705437)(573s)_CsLn_.pdf#page=449 Functional verification of power gated designs by compositional reasoning]”, Computer Aided Verification, Springer Berlin Heidelberg, pp. 433–445.</ref> रजिस्टर,<ref>P. C. Attie, H. Chockler, “[https://core.ac.uk/download/pdf/82434920.pdf Automatic verification of fault-tolerant register emulations]”, Electronic Notes in Theoretical Computer Science, vol. 149, no. 1, pp. 49–60.</ref> और IBM Power7 माइक्रोसंसाधक के सत्यापन<ref>K. D. Schubert, W. Roesner, J. M. Ludden, J. Jackson, J. Buchert, V. Paruthi, B. Brock, “[https://ieeexplore.ieee.org/abstract/document/5756329/ Functional verification of the IBM POWER7 microprocessor and POWER7 multiprocessor systems]”, IBM Journal of Research and Development, vol. 55, no 3.</ref> में औपचारिक तरीकों का इस्तेमाल किया है।

v t e कंप्यूटर विज्ञान
Note: This template roughly follows the 2012 ACM Computing Classification System.
हार्डवेयर	मुद्रित सर्किट बोर्ड परिधीय एकीकृत परिपथ बड़े पैमाने पर एकीकरण चिप पर सिस्टम (एसओसी) ऊर्जा की खपत (ग्रीन कंप्यूटिंग) इलेक्ट्रॉनिक डिजाइन स्वचालन हार्डवेयर एक्सिलरेशन
कंप्यूटर सिस्टम संगठन	कंप्यूटर आर्किटेक्चर अंतः स्थापित प्रणाली रीयल-टाइम कंप्यूटिंग निर्भरता
नेटवर्क	नेटवर्क आर्किटेक्चर नेटवर्क प्रोटोकॉल नेटवर्क घटक नेटवर्क अनुसूचक नेटवर्क प्रदर्शन मूल्यांकन नेटवर्क सेवा
सॉफ्टवेयर संगठन	दुभाषिया मध्यस्थ आभासी मशीन ऑपरेटिंग सिस्टम सॉफ्टवेयर गुणवत्ता
सॉफ्टवेयर नोटेशन और टूल्स	प्रोग्रामिंग प्रतिमान प्रोग्रामिंग भाषा संकलक डोमेन-विशिष्ट भाषा मॉडलिंग भाषा सॉफ्टवेयर फ्रेमवर्क समन्वित विकास पर्यावरण सॉफ्टवेयर विन्यास प्रबंधन सॉफ्टवेयर लाइब्रेरी सॉफ्टवेयर रिपोजिटरी
सॉफ्टवेयर डेवलपमेंट	नियंत्रण चर सॉफ्टवेयर विकास प्रक्रिया आवश्यकताओं के विश्लेषण सॉफ्टवेर डिज़ाइन सॉफ्टवेयर निर्माण सॉफ्टवेयर परिनियोजन सॉफ्टवेयर इंजीनियरिंग सॉफ्टवेयर की रखरखाव प्रोग्रामिंग टीम ओपन-सोर्स मॉडल
गणना का सिद्धांत	गणना का मॉडल औपचारिक भाषा ऑटोमेटा सिद्धांत कम्प्यूटेबिलिटी सिद्धांत कम्प्यूटेशनल जटिलता सिद्धांत तर्क शब्दार्थ
कलन विधि	एल्गोरिदम डिजाइन एल्गोरिदम का विश्लेषण एल्गोरिदमिक दक्षता यादृच्छिक एल्गोरिदम कम्प्यूटेशनल ज्यामिति
कंप्यूटिंग का गणित	गणित पृथक करें संभावना सांख्यिकी गणितीय सॉफ्टवेयर सूचना सिद्धांत गणितीय विश्लेषण संख्यात्मक विश्लेषण सैद्धांतिक कंप्यूटर विज्ञान
सूचना प्रणाली	डेटाबेस प्रबंधन प्रणाली सूचना भंडारण प्रणाली उद्यम सूचना प्रणाली सामाजिक सूचना प्रणाली भौगोलिक सूचना प्रणाली निर्णय समर्थन प्रणाली प्रक्रिया नियंत्रण प्रणाली मल्टीमीडिया सूचना प्रणाली डेटा माइनिंग डिजिटल लाइब्रेरी कंप्यूटिंग प्लेटफॉर्म डिजिटल विपणन वर्ल्ड वाइड वेब सूचना की पुनर्प्राप्ति
सुरक्षा	क्रिप्टोग्राफी औपचारिक तरीके सुरक्षा सेवाएं अतिक्रमण संसूचन प्रणाली हार्डवेयर सुरक्षा नेटवर्क सुरक्षा सूचना सुरक्षा आवेदन सुरक्षा
मानव-कंप्यूटर संपर्क	पारस्परिक प्रभाव वाली डिज़ाइन सामाजिक कंप्यूटिंग सर्वव्यापक कंप्यूटिंग विज़ुअलाइज़ेशन एक्सेसिबिलिटी
Concurrency	समवर्ती कंप्यूटिंग समानांतर कंप्यूटिंग वितरित अभिकलन मल्टीथ्रेडिंग मल्टीप्रोसेसिंग
कृत्रिम बुद्धि	प्राकृतिक भाषा प्रसंस्करण ज्ञान प्रतिनिधित्व और तर्क कंप्यूटर दृष्टी स्वचालित योजना और समय-निर्धारण खोज पद्धति नियंत्रण विधि कृत्रिम बुद्धि का दर्शन डिस्ट्रिब्यूटेड आर्टिफिशियल इंटेलिजेंस
मशीन लर्निंग	पर्यवेक्षित अध्ययन अनपर्यवेक्षित लर्निंग सुदृढीकरण सीखना बहु-कार्य सीखने क्रॉस-सत्यापन
ग्राफिक्स	एनिमेशन रेंडरिंग छवि हेरफेर ग्राफ़िक्स प्रोसेसिंग युनिट मिश्रित वास्तविकता आभासी वास्तविकता छवि संपीड़न सॉलिड मॉडलिंग
एप्लाइड कंप्यूटिंग	ई-कॉमर्स उपक्रम सॉफ्टवेयर कम्प्यूटेशनल गणित कम्प्यूटेशनल भौतिकी कम्प्यूटेशनल केमिस्ट्री कम्प्यूटेशनल बायोलॉजी कम्प्यूटेशनल सामाजिक विज्ञान कम्प्यूटेशनल इंजीनियरिंग कम्प्यूटेशनल हेल्थकेयर डिजिटल कला इलेक्ट्रॉनिक प्रकाशन सायबर युद्ध इलेक्ट्रॉनिक वोटिंग वीडियो गेम वर्ड प्रोसेसिंग संचालन अनुसंधान शैक्षिक प्रौद्योगिकी दस्तावेज़ प्रबंधन
Category Outline WikiProject Commons

Anonymous

Search

औपचारिक पद्यतियां: Difference between revisions

Namespaces

More

Page actions

Revision as of 08:56, 21 October 2022

Contents

पृष्ठभूमि

वर्गीकरण

हल्के औपचारिक तरीके

उपयोग

विशिष्टता

विकास

सत्यापन

साइन-ऑफ सत्यापन

मानव निर्देशित सबूत

स्वचालित प्रमाण

Applications

आवेदन

सॉफ्टवेयर विकास में

औपचारिक तरीके और संकेतन

विशिष्टता भाषाएं

मॉडल चेकर्स

संगठन

यह भी देखें

संदर्भ

इस पृष्ठ में अनुपलब्ध आंतरिक कड़ियों की सूची

अग्रिम पठन

बाहरी संबंध

Navigation

Navigation

Wiki tools

Wiki tools

Anonymous

Search

औपचारिक पद्यतियां: Difference between revisions

Revision as of 08:56, 21 October 2022

पृष्ठभूमि

वर्गीकरण

हल्के औपचारिक तरीके

उपयोग

विशिष्टता

विकास

सत्यापन

साइन-ऑफ सत्यापन

मानव निर्देशित सबूत

स्वचालित प्रमाण

Applications

आवेदन

सॉफ्टवेयर विकास में

औपचारिक तरीके और संकेतन

विशिष्टता भाषाएं

मॉडल चेकर्स

संगठन

यह भी देखें

संदर्भ

इस पृष्ठ में अनुपलब्ध आंतरिक कड़ियों की सूची

अग्रिम पठन

बाहरी संबंध

Navigation

Wiki tools

Page tools

Other projects

Categories