औपचारिक पद्यतियां

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

औपचारिक विधियाँ विभिन्न प्रकार के सैद्धांतिक कंप्यूटर विज्ञा के बुनियादी सिद्धांतों को नियोजित करती हैं, जिनमें तर्क गणना, औपचारिक भाषा, ऑटोमेटा सिद्धांत, नियंत्रण सिद्धांत, कार्यक्रम शब्दार्थ, प्रकार प्रणाली और प्रकार सिद्धांत सम्मिलित हैं।

पृष्ठभूमि

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

वर्गीकरण

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

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

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

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

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

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

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

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

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

उपयोग

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

विशिष्टता

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

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

विकास

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

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

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

पद्यतियां

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

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

साइन-ऑफ पद्यतियां

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

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

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

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

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

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

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

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

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

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

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

आवेदन

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

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

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

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

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

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

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

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

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

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

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

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

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

मॉडलचेकर्स

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

संगठन

• बीसीएस-एफएसीएस
• औपचारिक तरीके यूरोप
• जेड उपयोगकर्ता समूह

यह भी देखें

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

अग्रिम पठन

• 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.

बाहरी संबंध

• Formal Methods Europe (FME)
• Formal Methods Wiki
• Formal methods from Foldoc

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