औपचारिक विनिर्देश
कंप्यूटर विज्ञान में, औपचारिक विनिर्देश गणितीय रूप से आधारित तकनीकें है जिनका उद्देश्य प्रणाली और सॉफ़्टवेयर के कार्यान्वयन में सहायता करना होता है। उनका उपयोग एक प्रणाली का वर्णन करने, उसके व्यवहार का विश्लेषण करने और कठोर और प्रभावी तर्क उपकरणों के माध्यम से रुचि के प्रमुख गुणों की पुष्टि करके इसके डिजाइन में सहायता करने के लिए किया जाता है।[1][2] ये विनिर्देश इस अर्थ में औपचारिक है कि उनका एक वाक्य-विन्यास है, उनके शब्दार्थ एक डोमेन के भीतर आते है, और उपयोगी जानकारी का अनुमान लगाने के लिए उनका उपयोग किया जा सकता है।[3]
प्रेरणा
प्रत्येक गुजरते दशक में, कंप्यूटर प्रणाली तेजी से अधिक शक्तिशाली हो गए है और परिणामस्वरूप, वे समाज के लिए अधिक प्रभावशाली बन गए है। इस वजह से, विश्वसनीय सॉफ़्टवेयर के डिज़ाइन और कार्यान्वयन में सहायता के लिए बेहतर तकनीकों की आवश्यकता है। स्थापित अभियंत्रिकी अनुशासन उत्पाद डिजाइन बनाने और मान्य करने की नींव के रूप में गणितीय विश्लेषण का उपयोग करते है। औपचारिक विनिर्देश सॉफ्टवेयर अभियंत्रिकी विश्वसनीयता में इसे प्राप्त करने का एक ऐसी विधि है जैसे कि एक बार भविष्यवाणी की गई थी। कोड की गुणवत्ता बढ़ाने के लिए सामान्यतः सॉफ़्टवेयर परीक्षण जैसे अन्य तरीकों का अधिक उपयोग किया जाता है।[1]
उपयोग
इस तरह के एक विनिर्देश को देखते हुए, यह प्रदर्शित करने के लिए औपचारिक सत्यापन तकनीकों का उपयोग करना संभव है कि एक प्रणाली डिज़ाइन अपने विनिर्देश के संबंध में सही है। यह किसी भी बड़े निवेश को वास्तविक कार्यान्वयन में किए जाने से पहले गलत प्रणाली डिज़ाइन को संशोधित करने की अनुमति देता है। एक अन्य दृष्टिकोण एक विनिर्देश को एक डिजाइन में बदलने के लिए संभवतः सही शोधन चरणों का उपयोग करना है, जो अंततः एक कार्यान्वयन में परिवर्तित हो जाता है जो निर्माण द्वारा सही होता है।
यह ध्यान रखना महत्वपूर्ण है कि एक औपचारिक विनिर्देश एक कार्यान्वयन नहीं है, जबकि इसका उपयोग कार्यान्वयन को विकसित करने के लिए किया जा सकता है। औपचारिक विनिर्देश वर्णन करते है कि प्रणाली को क्या करना चाहिए, न कि प्रणाली को कैसे करना चाहिए।
एक अच्छे विनिर्देशन में निम्नलिखित में से कुछ विशेषताएँ होनी चाहिए: पर्याप्त, आंतरिक रूप से सुसंगत, स्पष्ट, पूर्ण, संतुष्ट, न्यूनतम[3]
एक अच्छे विनिर्देशन में होगा:[3]
* निर्माण क्षमता, प्रबंधनीयता और विकास
- उपयोगिता
- संप्रेषणीयता
- शक्तिशाली और कुशल विश्लेषण
औपचारिक विशिष्टताओं में रुचि होने का एक मुख्य कारण यह है कि वे सॉफ्टवेयर कार्यान्वयन पर प्रूफ करने की क्षमता प्रदान करते है।[2] इन प्रमाणों का उपयोग किसी विनिर्देश को मान्य करने, डिज़ाइन की शुद्धता को सत्यापित करने, या यह साबित करने के लिए किया जा सकता है कि कोई प्रोग्राम किसी विनिर्देश को पूरा करता है।[2]
सीमाएं
एक डिजाइन (या कार्यान्वयन) को कभी भी "सही" घोषित नहीं किया जा सकता है। यह केवल "किसी दिए गए विनिर्देश के संबंध में सही" हो सकता है। क्या औपचारिक विनिर्देश हल की जाने वाली समस्या का सही वर्णन करता है, यह एक अलग मुद्दा है। यह संबोधित करने के लिए भी एक कठिन मुद्दा है क्योंकि यह अंततः एक अनौपचारिक ठोस समस्या डोमेन के अमूर्त औपचारिक प्रतिनिधित्व के निर्माण की समस्या से संबंधित है, और इस तरह के अमूर्त कदम औपचारिक प्रमाण के लिए उपयुक्त नहीं है। चूंकि, उन गुणों से संबंधित "चुनौती" प्रमेयों को साबित करके एक विनिर्देश को मान्य करना संभव है जो विनिर्देश प्रदर्शित करने की अपेक्षा करते है। यदि सही है, तो ये प्रमेय विनिर्देशक की विशिष्टता की समझ और अंतर्निहित समस्या डोमेन के साथ उसके संबंध को सुदृढ़ करते है। यदि नहीं, तो विनिर्देशन को उत्पादन (और कार्यान्वयन) के साथ सम्मलित लोगों की डोमेन समझ को बेहतर ढंग से प्रतिबंधित करने के लिए विनिर्देश को बदलने की आवश्यकता है।
सॉफ्टवेयर विकास के औपचारिक विधि उद्योग में व्यापक रूप से उपयोग नहीं किए जाते है। अधिकांश कंपनियां उन्हें अपनी सॉफ्टवेयर विकास प्रक्रियाओं में लागू करने के लिए लागत प्रभावी नहीं मानती है।[4] इसके कई कारण हो सकते है, जिनमें से कुछ है:
- समय
- कम मापने योग्य रिटर्न के साथ उच्च प्रारंभिक स्टार्ट अप लागत
- लचीलापन
- बहुत सारी सॉफ्टवेयर कंपनियाँ चुस्त सॉफ्टवेयर विकास का उपयोग करती है जो लचीलेपन पर ध्यान केंद्रित करती है। पूरी प्रणाली के सामने औपचारिक विनिर्देश करना अधिकांशतः लचीलेपन के विपरीत माना जाता है। चूंकि, "फुर्तीला" विकास के साथ औपचारिक विशिष्टताओं का उपयोग करने के लाभों में कुछ शोध होता है
- जटिलता
- उन्हें प्रभावी ढंग से समझने और लागू करने के लिए उच्च स्तर की गणितीय विशेषज्ञता और विश्लेषणात्मक कौशल की आवश्यकता होती है
- इसका समाधान उपकरण और मॉडल विकसित करना होता है जो इन तकनीकों को लागू करने की अनुमति देता है लेकिन अंतर्निहित गणित को छुपाता है[2]
- कम कार्य क्षेत्र[3]
- वे परियोजना में सभी हितधारकों के लिए ब्याज की संपत्तियों पर कब्जा नहीं करते है[3]
- वे यूजर इंटरफेस और यूजर इंटरेक्शन को निर्दिष्ट करने का अच्छा काम नहीं करते है[4]
- लागत प्रभावी नहीं
- यह पूरी तरह से सच नहीं है, उनके उपयोग को केवल महत्वपूर्ण प्रणालियों के मुख्य भागों तक सीमित करके उन्होंने लागत प्रभावी दिखाया है[4]
अन्य सीमाएँ:[3]
एकांत
- निम्न-स्तरीय ऑन्कोलॉजी
- खराब मार्गदर्शन
- चिंताओं का खराब अलगाव
- खराब टूल फीडबैक
उदाहरण
औपचारिक विनिर्देश तकनीकें अधिक समय से विभिन्न डोमेन और विभिन्न पैमानों पर उपस्तिथ होते है।[5] औपचारिक विशिष्टताओं के कार्यान्वयन इस बात पर निर्भर करते हुए भिन्न होंगे कि वे किस प्रकार की प्रणाली को मॉडल बनाने का प्रयास कर रहे है, उन्हें कैसे लागू किया जाता है और सॉफ़्टवेयर जीवन चक्र के किस बिंदु पर उन्हें प्रस्तुत किया गया है।[2] इस प्रकार के मॉडलों को निम्नलिखित विनिर्देश प्रतिमानों में वर्गीकृत किया जा सकता है:
- इतिहास-आधारित विनिर्देश[3]
- प्रणाली इतिहास पर आधारित व्यवहार
- कथनों की व्याख्या समय के साथ की जाती है
- राज्य आधारित विनिर्देश[3]
- प्रणाली स्टेट्स पर आधारित व्यवहार
- अनुक्रमिक चरणों की श्रृंखला
- जेड अंकन, वियना विकास पद्धति या बी-विधि जैसी भाषाएं इस प्रतिमान पर भरोसा करती है[3]
- संक्रमण-आधारित विनिर्देश[3]
- प्रणाली के राज्य से राज्य के संक्रमण के आधार पर व्यवहार
- एक प्रतिक्रियाशील प्रणाली के साथ सबसे अच्छा उपयोग किया जाता है
- स्टेटचार्ट्स, प्रोमेला, स्टेप-एसपीएल, आरएसएमएल या एससीआर जैसी भाषाएँ इस प्रतिमान पर भरोसा करती है[3]
- कार्यात्मक विनिर्देश[3]
- गणितीय कार्यों की संरचना के रूप में एक प्रणाली निर्दिष्ट करें
- ओबीजे, एएसएल, प्लस, लार्च, एचओएल या पीवीएस इस प्रतिमान पर भरोसा करते है[3]
- परिचालन विशिष्टता[3]
- शुरुआती भाषाएँ जैसे पैस्ले (प्रोग्रामिंग लैंग्वेज), जीआईएसटी, पेट्री नेट या प्रोसेस अल्जेब्रा इस प्रतिमान पर निर्भर करती है[3]
उपरोक्त प्रतिमानों के अतिरिक्त, इन विशिष्टताओं के निर्माण में सुधार करने में सहायता के लिए कुछ ह्यूरिस्टिक्स लागू करने के विधि है। यहां संदर्भित पेपर विनिर्देश डिजाइन करते समय उपयोग करने के लिए ह्यूरिस्टिक्स पर सबसे अच्छी चर्चा करता है।[5] वे एक विभाजन और जीत एल्गोरिथम लागू करके ऐसा करते है |
सॉफ्टवेयर उपकरण
जेड नोटेशन एक प्रमुख औपचारिक विनिर्देशन भाषा का एक उदाहरण है। अन्य में विएना विकास पद्धति की विशिष्टता भाषा (वीडीएम-एसएल) और बी-विधि की सार मशीन संकेतन (एएमएन) सम्मलित होती है। वेब सेवा क्षेत्र में, गैर-कार्यात्मक गुणों का वर्णन करने के लिए अधिकांशतः औपचारिक विनिर्देश का उपयोग किया जाता है।[6]
कुछ उपकरण है:[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 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
