औपचारिक तरीके

From alpha
Jump to navigation Jump to search

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


पृष्ठभूमि

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


टैक्सोनॉमी

औपचारिक तरीकों का उपयोग कई स्तरों पर किया जा सकता है:

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

इस पर आगे की जानकारी #उपयोग विस्तृत है।

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

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

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

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


उपयोग करता है

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

विशिष्टता

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

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

विकास

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

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

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

सत्यापन

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

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

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

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

मानव निर्देशित प्रमाण

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

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

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

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

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

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

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

आलोचकों ने ध्यान दिया कि उनमें से कुछ प्रणालियाँ Oracle मशीनों की तरह हैं: वे सत्य की घोषणा करती हैं, फिर भी उस सत्य की कोई व्याख्या नहीं करती हैं। Quis custodiet ipsos custodes की भी समस्या है? ; यदि कार्यक्रम जो सत्यापन में सहायता करता है स्वयं अप्रमाणित है, तो उत्पादित परिणामों की सुदृढ़ता पर संदेह करने का कारण हो सकता है। कुछ आधुनिक मॉडल जाँच उपकरण अपने प्रमाण में प्रत्येक चरण का विवरण देते हुए एक प्रूफ लॉग का उत्पादन करते हैं, जिससे उपयुक्त उपकरण दिए जाने पर, स्वतंत्र सत्यापन करना संभव हो जाता है।

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

अनुप्रयोग

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

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


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

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

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

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

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

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

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

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

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

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

रेज़ विनिर्देश भाषा बढ़ाएं

मॉडल चेकर्स

Main article: List of model checking tools

संगठन

Main page: Category:Formal methods organizations

यह भी देखें

संदर्भ

  1. ↑ Butler, R. W. (2001-08-06). "What is Formal Methods?". Retrieved 2006-11-16.
  2. ↑ Holloway, C. Michael. "इंजीनियरों को औपचारिक तरीकों पर विचार क्यों करना चाहिए" (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. ↑ "एटेलियर बी". www.atelierb.eu.
  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[permanent dead link]", 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.org.


अग्रिम पठन


बाहरी संबंध

Archival material
Retrieved from "https://alpha.indicwiki.in/index.php?title=औपचारिक_तरीके&oldid=194521"