औपचारिक विनिर्देश
कंप्यूटर विज्ञान में, औपचारिक विनिर्देश गणितीय रूप से आधारित तकनीकें हैं जिनका उद्देश्य सिस्टम और सॉफ़्टवेयर के कार्यान्वयन में सहायता करना है। उनका उपयोग एक प्रणाली का वर्णन करने, उसके व्यवहार का विश्लेषण करने और कठोर और प्रभावी तर्क उपकरणों के माध्यम से रुचि के प्रमुख गुणों की पुष्टि करके इसके डिजाइन में सहायता के लिए किया जाता है।[1][2] ये विनिर्देश इस अर्थ में औपचारिक हैं कि उनके पास एक वाक्य-विन्यास है, उनके शब्दार्थ एक डोमेन के भीतर आते हैं, और उपयोगी जानकारी का अनुमान लगाने के लिए उनका उपयोग किया जा सकता है।[3]
प्रेरणा
प्रत्येक गुजरते दशक में, कंप्यूटर सिस्टम तेजी से अधिक शक्तिशाली हो गए हैं और परिणामस्वरूप, वे समाज के लिए अधिक प्रभावशाली बन गए हैं। इस वजह से, विश्वसनीय सॉफ़्टवेयर के डिज़ाइन और कार्यान्वयन में सहायता के लिए बेहतर तकनीकों की आवश्यकता है। स्थापित इंजीनियरिंग अनुशासन उत्पाद डिजाइन बनाने और मान्य करने की नींव के रूप में गणितीय विश्लेषण का उपयोग करते हैं। औपचारिक विनिर्देश सॉफ्टवेयर इंजीनियरिंग विश्वसनीयता में इसे प्राप्त करने का एक ऐसा तरीका है जैसा कि एक बार भविष्यवाणी की गई थी। कोड की गुणवत्ता बढ़ाने के लिए सॉफ़्टवेयर परीक्षण जैसे अन्य तरीकों का अधिक सामान्यतः उपयोग किया जाता है।[1]
उपयोग करता है
इस तरह के एक विनिर्देश को देखते हुए, यह प्रदर्शित करने के लिए औपचारिक सत्यापन तकनीकों का उपयोग करना संभव है कि एक सिस्टम डिज़ाइन इसकी विशिष्टता के संबंध में शुद्धता (कंप्यूटर विज्ञान) है। यह किसी भी बड़े निवेश को वास्तविक कार्यान्वयन में किए जाने से पहले गलत सिस्टम डिज़ाइन को संशोधित करने की अनुमति देता है। एक अन्य दृष्टिकोण एक विनिर्देश को एक डिज़ाइन में बदलने के लिए संभवतः सही प्रोग्राम शोधन चरणों का उपयोग करना है, जो अंततः एक कार्यान्वयन में परिवर्तित हो जाता है जो निर्माण द्वारा सही होता है।
यह ध्यान रखना महत्वपूर्ण है कि एक औपचारिक विनिर्देश एक कार्यान्वयन नहीं है, बल्कि इसका उपयोग कार्यान्वयन को विकसित करने के लिए किया जा सकता है। औपचारिक विनिर्देश वर्णन करते हैं कि सिस्टम को क्या करना चाहिए, न कि सिस्टम को कैसे करना चाहिए।
एक अच्छे विनिर्देशन में निम्नलिखित में से कुछ विशेषताएँ होनी चाहिए: पर्याप्त, आंतरिक रूप से सुसंगत, स्पष्ट, पूर्ण, संतुष्ट, न्यूनतम[3]
एक अच्छे विनिर्देशन में होगा:[3]* निर्माण क्षमता, प्रबंधनीयता और विकास
- उपयोगिता
- संप्रेषणीयता
- शक्तिशाली और कुशल विश्लेषण
औपचारिक विशिष्टताओं में रुचि होने का एक मुख्य कारण यह है कि वे सॉफ्टवेयर कार्यान्वयन पर प्रूफ करने की क्षमता प्रदान करेंगे।[2]इन प्रमाणों का उपयोग किसी विनिर्देश को मान्य करने, डिज़ाइन की शुद्धता को सत्यापित करने, या यह साबित करने के लिए किया जा सकता है कि कोई प्रोग्राम किसी विनिर्देश को पूरा करता है।[2]
सीमाएं
एक डिजाइन (या कार्यान्वयन) को कभी भी "सही" घोषित नहीं किया जा सकता है। यह केवल "किसी दिए गए विनिर्देश के संबंध में सही" हो सकता है। क्या औपचारिक विनिर्देश हल की जाने वाली समस्या का सही वर्णन करता है, यह एक अलग मुद्दा है। यह संबोधित करने के लिए भी एक कठिन मुद्दा है क्योंकि यह अंततः एक अनौपचारिक ठोस डोमेन (सॉफ्टवेयर इंजीनियरिंग) के अमूर्त औपचारिक प्रतिनिधित्व के निर्माण की समस्या से संबंधित है, और इस तरह के अमूर्त कदम औपचारिक प्रमाण के लिए उत्तरदायी नहीं हैं। हालांकि, विशेषताओं से संबंधित "चुनौती" प्रमेयों को साबित करके एक विनिर्देश को सत्यापित और मान्य करना संभव है, जो कि विनिर्देश प्रदर्शित करने की उम्मीद है। यदि सही है, तो ये प्रमेय विनिर्देशक की विशिष्टता की समझ और अंतर्निहित समस्या डोमेन के साथ उसके संबंध को सुदृढ़ करते हैं। यदि नहीं, तो विनिर्देशों को उत्पादन (और कार्यान्वयन) के साथ शामिल लोगों की डोमेन समझ को बेहतर ढंग से प्रतिबिंबित करने के लिए विनिर्देश को बदलने की आवश्यकता है।
सॉफ्टवेयर विकास के औपचारिक तरीके उद्योग में व्यापक रूप से उपयोग नहीं किए जाते हैं। अधिकांश कंपनियां उन्हें अपनी सॉफ्टवेयर विकास प्रक्रियाओं में लागू करने के लिए लागत प्रभावी नहीं मानती हैं।[4] इसके कई कारण हो सकते हैं, जिनमें से कुछ हैं:
- समय
- कम मापने योग्य रिटर्न के साथ उच्च प्रारंभिक स्टार्ट अप लागत
- लचीलापन
- बहुत सारी सॉफ्टवेयर कंपनियां चुस्त सॉफ्टवेयर विकास का उपयोग करती हैं जो लचीलेपन पर ध्यान केंद्रित करता है। पूरी प्रणाली के सामने औपचारिक विनिर्देश करना अक्सर लचीलेपन के विपरीत माना जाता है। हालांकि, फुर्तीले विकास के साथ औपचारिक विशिष्टताओं का उपयोग करने के लाभों पर कुछ शोध किया गया है रेफ नाम = p14-नंबर मेश >Nummenmaa, Timo; Tiensuu, Aleksi; Berki, Eleni; Mikkonen, Tommi; Kuittinen, Jussi; Kultima, Annakaisa (4 August 2011). "निष्पादन योग्य औपचारिक विशिष्टताओं के साथ प्राकृतिक उपयोगकर्ता सहभागिता को सुगम बनाकर चुस्त विकास का समर्थन करना". ACM SIGSOFT Software Engineering Notes. 36 (4): 1–10. doi:10.1145/1988997.2003643. S2CID 2139235.</ref>
- जटिलता
- उन्हें प्रभावी ढंग से समझने और लागू करने के लिए उच्च स्तर की गणितीय विशेषज्ञता और विश्लेषणात्मक कौशल की आवश्यकता होती है[5]
- इसका समाधान उपकरण और मॉडल विकसित करना होगा जो इन तकनीकों को लागू करने की अनुमति देता है लेकिन अंतर्निहित गणित को छुपाता है[2][5]* कम कार्य क्षेत्र[3]** वे परियोजना में सभी आवश्यकताओं के विश्लेषण # हितधारक की पहचान के लिए रुचि के गुणों पर कब्जा नहीं करते हैं[3]** वे यूजर इंटरफेस और यूजर इंटरेक्शन को निर्दिष्ट करने का अच्छा काम नहीं करते हैं[4]* लागत प्रभावी नहीं
- यह पूरी तरह से सच नहीं है, उनके उपयोग को केवल महत्वपूर्ण प्रणालियों के मुख्य भागों तक सीमित करके उन्होंने लागत प्रभावी दिखाया है[4]
अन्य सीमाएँ:[3]* एकांत
- निम्न-स्तरीय ऑन्कोलॉजी
- खराब मार्गदर्शन
- चिंताओं का खराब अलगाव
- खराब टूल फीडबैक
प्रतिमान
औपचारिक विनिर्देश तकनीकें काफी समय से विभिन्न डोमेन और विभिन्न पैमानों पर मौजूद हैं।[6] औपचारिक विनिर्देशों के कार्यान्वयन इस बात पर निर्भर करते हुए भिन्न होंगे कि वे किस प्रकार की प्रणाली को मॉडल करने का प्रयास कर रहे हैं, उन्हें कैसे लागू किया जाता है और सॉफ़्टवेयर जीवन चक्र के किस बिंदु पर उन्हें पेश किया गया है।[2]इस प्रकार के मॉडलों को निम्नलिखित विनिर्देश प्रतिमानों में वर्गीकृत किया जा सकता है:
- इतिहास-आधारित विनिर्देश[3]** सिस्टम इतिहास पर आधारित व्यवहार
- कथनों की व्याख्या समय के साथ की जाती है
- राज्य आधारित विनिर्देश[3]** सिस्टम स्टेट्स पर आधारित व्यवहार
- अनुक्रमिक चरणों की श्रृंखला, (उदाहरण के लिए एक वित्तीय लेनदेन)
- जेड अंकन, वियना विकास पद्धति या बी-विधि जैसी भाषाएं इस प्रतिमान पर भरोसा करती हैं[3]* संक्रमण-आधारित विनिर्देश[3]** प्रणाली के राज्य से राज्य के संक्रमण के आधार पर व्यवहार
- एक प्रतिक्रियाशील प्रणाली के साथ सबसे अच्छा उपयोग किया जाता है
- Statecharts, PROMELA, STeP-SPL, RSML या SCR जैसी भाषाएँ इस प्रतिमान पर भरोसा करती हैं[3]* कार्यात्मक विनिर्देश[3]** गणितीय कार्यों की संरचना के रूप में एक प्रणाली निर्दिष्ट करें
- OBJ, ASL, PLUSS, LARCH, HOL या PVS इस प्रतिमान पर भरोसा करते हैं[3]* परिचालन विशिष्टता[3]** शुरुआती भाषाएँ जैसे पैस्ले (प्रोग्रामिंग लैंग्वेज), जीआईएसटी, पेट्री नेट या प्रोसेस अल्जेब्रा इस प्रतिमान पर निर्भर करती हैं[3]
उपरोक्त प्रतिमानों के अतिरिक्त, इन विशिष्टताओं के निर्माण में सुधार करने में सहायता के लिए कुछ ह्यूरिस्टिक्स लागू करने के तरीके हैं। यहां संदर्भित पेपर विनिर्देश डिजाइन करते समय उपयोग करने के लिए ह्यूरिस्टिक्स पर सबसे अच्छी चर्चा करता है।[6]वे एक विभाजन और जीत एल्गोरिथम लागू करके ऐसा करते हैं | फूट डालो और जीतो दृष्टिकोण।
सॉफ्टवेयर उपकरण
जेड नोटेशन एक प्रमुख औपचारिक विनिर्देशन भाषा का एक उदाहरण है। अन्य में विएना विकास पद्धति की विशिष्टता भाषा (वीडीएम-एसएल) और बी-विधि की सार मशीन संकेतन (एएमएन) शामिल हैं। वेब सेवा क्षेत्र में, गैर-कार्यात्मक गुणों का वर्णन करने के लिए अक्सर औपचारिक विनिर्देश का उपयोग किया जाता है[7] (वेब सेवाओं की सेवा की गुणवत्ता)।
कुछ उपकरण हैं:[4]
- बीजीय
- मॉडल आधारित
- # जेड नोटेशन
- बी-विधि
- वियना विकास पद्धति
- अनुक्रमिक प्रक्रियाओं का संचार करना
- पेट्री नेट
- टीएलए+
यह भी देखें
- बीजगणितीय विनिर्देश
- औपचारिक तरीके
- मॉडल-आधारित विनिर्देश
- सॉफ्टवेयर इंजीनियरिंग
- विशिष्टता भाषा
- विशिष्टता (तकनीकी मानक)
संदर्भ
- ↑ 1.0 1.1 Hierons, R. M.; Bogdanov, K.; Bowen, J. P.; Cleaveland, R.; Derrick, J.; Dick, J.; Gheorghe, M.; Harman, M.; Kapoor, K.; Krause, P.; Lüttgen, G.; Simons, A. J. H.; Vilkomir, S. A.; Woodward, M. R.; Zedan, H. (2009). "परीक्षण का समर्थन करने के लिए औपचारिक विनिर्देशों का उपयोग करना". ACM Computing Surveys. 41 (2): 1. CiteSeerX 10.1.1.144.3320. doi:10.1145/1459352.1459354. S2CID 10686134.
- ↑ 2.0 2.1 2.2 2.3 2.4 Gaudel, M.-C. (1994). "Formal specification techniques". Proceedings of 16th International Conference on Software Engineering. pp. 223–227. doi:10.1109/ICSE.1994.296781. ISBN 978-0-8186-5855-6. S2CID 60740848.
- ↑ 3.00 3.01 3.02 3.03 3.04 3.05 3.06 3.07 3.08 3.09 3.10 3.11 3.12 3.13 3.14 Lamsweerde, A. V. (2000). "Formal specification". सॉफ्टवेयर इंजीनियरिंग के भविष्य पर सम्मेलन की कार्यवाही - आईसीएसई '00. pp. 147–159. doi:10.1145/336512.336546. ISBN 978-1581132533. S2CID 4657483.
- ↑ 4.0 4.1 4.2 4.3 Sommerville, Ian (2009). "औपचारिक विशिष्टता" (PDF). Software Engineering. Retrieved 3 February 2013.
- ↑ 5.0 5.1 Cite error: Invalid
<ref>tag; no text was provided for refs namedp14-nummenmaasen - ↑ 6.0 6.1 van der Poll, John A.; Paula Kotze (2002). "What design heuristics may enhance the utility of a formal specification?". Proceedings of the 2002 Annual Research Conference of the South African Institute of Computer Scientists and Information Technologists on Enablement Through Technology. SAICSIT '02: 179–194. ISBN 9781581135961.
- ↑ S-Cube Knowledge Model: Formal Specification
बाहरी संबंध
- A Case for Formal Specification (Technology) Archived 2005-10-21 at the Wayback Machine by Coryoth 2005-07-30
