पहुंच क्षमता विश्लेषण

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

सिंहावलोकन

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

रीचैबिलिटी विश्लेषण के लिए, स्थानीय संस्थाओं को उनके राज्यों और संक्रमणों द्वारा प्रतिरूपित किया जाता है। एक इकाई जब संदेश भेजती है, प्राप्त संदेश का उपभोग करती है, या अपने स्थानीय सेवा इंटरफ़ेस पर एक सहभागिता करती है, तो स्थिति बदल जाती है। वैश्विक राज्य $s=(s_{1},s_{2},...,s_{n},medium)$ n संस्थाओं के साथ एक प्रणाली का ^[3] राज्यों द्वारा निर्धारित किया जाता है $s_{i}$ (i=1, ... n) संस्थाओं और संचार की स्थिति $medium$ . सबसे सरल मामले में, दो संस्थाओं के बीच का माध्यम विपरीत दिशाओं में दो FIFO कतारों द्वारा प्रतिरूपित किया जाता है, जिसमें पारगमन में संदेश होते हैं (जो भेजे जाते हैं, लेकिन अभी तक उपभोग नहीं किए जाते हैं)। रीचैबिलिटी विश्लेषण संस्थाओं के राज्य संक्रमण के सभी संभावित अनुक्रमों का विश्लेषण करके वितरित प्रणाली के संभावित व्यवहार पर विचार करता है, और संबंधित वैश्विक राज्यों तक पहुंच गया है।^[4] रीचैबिलिटी एनालिसिस का नतीजा एक ग्लोबल स्टेट ट्रांजिशन ग्राफ (जिसे रीचैबिलिटी ग्राफ भी कहा जाता है) है, जो डिस्ट्रीब्यूटेड सिस्टम की सभी ग्लोबल स्टेट्स को दिखाता है, जो शुरुआती ग्लोबल स्टेट से रीचेबल हैं, और लोकल द्वारा किए गए सेंड, कंज्यूम और सर्विस इंटरैक्शन के सभी संभावित सीक्वेंस हैं। संस्थाओं। हालाँकि, कई मामलों में यह संक्रमण ग्राफ असीम है और इसे पूरी तरह से नहीं खोजा जा सकता है। ट्रांज़िशन ग्राफ़ का उपयोग प्रोटोकॉल के सामान्य डिज़ाइन दोषों की जाँच के लिए किया जा सकता है (नीचे देखें), लेकिन यह भी सत्यापित करने के लिए कि संस्थाओं द्वारा सेवा इंटरैक्शन के अनुक्रम सिस्टम के वैश्विक सेवा विनिर्देश द्वारा दी गई आवश्यकताओं के अनुरूप हैं।^[1]

प्रोटोकॉल गुण

बाउंडेडनेस: यदि ट्रांज़िट में हो सकने वाले संदेशों की संख्या बाउंडेड है और सभी संस्थाओं की संख्या स्टेट्स बाउंडेड हैं, तो ग्लोबल स्टेट ट्रांज़िशन ग्राफ़ बाउंडेड है। सवाल यह है कि परिमित राज्य संस्थाओं के मामले में संदेशों की संख्या सीमित रहती है या नहीं, यह सामान्य अनिर्णीत समस्या है।^[5] जब ट्रांज़िट में संदेशों की संख्या दी गई सीमा तक पहुंच जाती है, तो आमतौर पर ट्रांज़िशन ग्राफ़ के अन्वेषण को छोटा कर दिया जाता है.

निम्नलिखित डिज़ाइन दोष हैं:

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

एक उदाहरण

आरेख दो प्रोटोकॉल संस्थाओं और उनके बीच आदान-प्रदान किए गए संदेशों को दिखाता है।

आरेख दो परिमित राज्य मशीनों को दिखाता है जो संबंधित प्रोटोकॉल संस्थाओं के गतिशील व्यवहार को परिभाषित करते हैं।

यह आरेख दो प्रोटोकॉल संस्थाओं और उनके बीच संदेशों के आदान-प्रदान के लिए उपयोग किए जाने वाले दो फीफो चैनलों से युक्त वैश्विक प्रणाली का एक राज्य मशीन मॉडल दिखाता है।

एक उदाहरण के रूप में, हम दो प्रोटोकॉल संस्थाओं की प्रणाली पर विचार करते हैं जो संदेश ma, mb, mc और md को एक दूसरे के साथ आदान-प्रदान करती हैं, जैसा कि पहले आरेख में दिखाया गया है। प्रोटोकॉल को दो संस्थाओं के व्यवहार से परिभाषित किया गया है, जो दूसरे आरेख में दो राज्य मशीनों के रूप में दिया गया है। यहाँ प्रतीक! मतलब संदेश भेजना, और ? एक प्राप्त संदेश का उपभोग करने का मतलब है। प्रारंभिक राज्य राज्य हैं 1।

तीसरा आरेख वैश्विक राज्य मशीन के रूप में इस प्रोटोकॉल के लिए पुन: योग्यता विश्लेषण का परिणाम दिखाता है। प्रत्येक वैश्विक स्थिति में चार घटक होते हैं: प्रोटोकॉल इकाई A (बाएं), इकाई B की स्थिति (दाएं) और मध्य में पारगमन में संदेश (ऊपरी भाग: A से B तक; निचला भाग: B से A तक) ). इस वैश्विक राज्य मशीन का प्रत्येक संक्रमण प्रोटोकॉल इकाई ए या इकाई बी के एक संक्रमण से मेल खाता है। प्रारंभिक अवस्था [1, -, 1] है (पारगमन में कोई संदेश नहीं)।

एक देखता है कि इस उदाहरण में एक वैश्विक स्थिति स्थान है - संदेशों की अधिकतम संख्या जो एक ही समय में ट्रांज़िट में हो सकती है, दो है। इस प्रोटोकॉल में एक वैश्विक गतिरोध है, जो राज्य [2, - -, 3] है। यदि कोई उपभोग संदेश एमबी के लिए राज्य 2 में ए के संक्रमण को हटा देता है, तो वैश्विक राज्यों [2, एमए एमबी, 3] और [2, - एमबी, 3] में एक अनिर्दिष्ट स्वागत होगा।

संदेश संचरण

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

इस बारे में अलग-अलग धारणाएँ बनाई गई हैं कि क्या कोई इकाई उपभोग के लिए किसी विशेष संदेश का चयन कर सकती है जब कई संदेश आ चुके हों और उपभोग के लिए तैयार हों। मूल मॉडल निम्नलिखित हैं:

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

अनिर्दिष्ट रिसेप्शन की समस्या की पहचान करने वाला मूल पेपर,^[6] और बाद के अधिकांश कार्य, एकल इनपुट कतार मान लिए गए।^[7] कभी-कभी, दौड़ की स्थिति द्वारा अनिर्दिष्ट रिसेप्शन पेश किए जाते हैं, जिसका अर्थ है कि दो संदेश प्राप्त होते हैं और उनका क्रम परिभाषित नहीं होता है (जो अक्सर होता है यदि वे अलग-अलग भागीदारों से आते हैं)। जब कई क्यू या रिसेप्शन पूल का उपयोग किया जाता है तो इनमें से कई डिज़ाइन दोष गायब हो जाते हैं।^[8] रिसेप्शन पूल के व्यवस्थित उपयोग के साथ, रीचैबिलिटी विश्लेषण को आंशिक डेडलॉक और पूल में हमेशा के लिए शेष संदेशों की जांच करनी चाहिए (इकाई द्वारा उपभोग किए बिना) ^[9]

व्यावहारिक मुद्दे

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

पहुंच योग्यता विश्लेषण का एक व्यावहारिक मुद्दा तथाकथित "राज्य अंतरिक्ष विस्फोट" है। यदि किसी प्रोटोकॉल की दो संस्थाओं में प्रत्येक में 100 अवस्थाएँ हैं, और माध्यम में 10 प्रकार के संदेश शामिल हो सकते हैं, प्रत्येक दिशा में दो तक, तो पहुँच योग्यता ग्राफ में वैश्विक राज्यों की संख्या 100 x 100 x (10) संख्या से बंधी है x 10) x (10 x 10) जो 100 मिलियन है। इसलिए रीचैबिलिटी ग्राफ पर रीचैबिलिटी एनालिसिस और मॉडल चेकिंग को स्वचालित रूप से करने के लिए कई टूल विकसित किए गए हैं। हम केवल दो उदाहरणों का उल्लेख करते हैं: SPIN मॉडल चेकर और वितरित प्रक्रियाओं के निर्माण और विश्लेषण के लिए एक टूलबॉक्स।

अग्रिम पठन

Communication protocols
Gerald Holzmann: Design and Validation of Computer Protocols, Prentice Hall, 1991.
G.v. Bochmann, D. Rayner and C.H. West: Some notes on the history of protocol engineering, Computer Networks journal, 54 (2010), pp 3197–3209.

संदर्भ और नोट्स

↑ ^1.0 ^1.1 Bochmann, G.v. "Finite State Description of Communication Protocols, Computer Networks, Vol. 2 (1978), pp. 361-372". {{cite journal}}: Cite journal requires |journal= (help)
↑ K.A. Bartlett, R.A. Scantlebury and P.T. Wilkinson, A note on reliable full-duplex transmission over half- duplex links, C.ACM 12, 260 (1969).
↑ Note: In the case of protocol analysis, there are normally only two entities.
↑ Note: The corruption or loss of a message is modeled as a state transition of the $medium$ .
↑ M.G.Gouda, E.G.Manning, Y.T.Yu: On the progress of communication between two finite state machines, doi
↑ P. Zafiropulo, C. West, H. Rudin, D. Cowan, D. Brand : Towards analyzing and synthesizing protocols, IEEE Transactions on Communications ( Volume: 28, Issue: 4, Apr 1980 )
↑ Note: The SAVE construct of SDL can be used to indicate that certain types of messages should not be consumed in the current state, but saved for future processing.
↑ M.F. Al-hammouri and G.v. Bochmann : Realizability of service specifications, Proc. System Analysis and Modelling (SAM) conference 2018, Copenhagen, LNCS, Springer
↑ C. Fournet, T. Hoare, S. K. Rajamani, and J. Rehof : Stuck-free Conformance, Proc. 16th Intl. Conf. on Computer Aided Verification (CAV’04), LNCS, vol. 3114, Springer, 2004

[Boch78-1] 1.0 ^1.1 Bochmann, G.v. "Finite State Description of Communication Protocols, Computer Networks, Vol. 2 (1978), pp. 361-372". {{cite journal}}: Cite journal requires |journal= (help)

[2] K.A. Bartlett, R.A. Scantlebury and P.T. Wilkinson, A note on reliable full-duplex transmission over half- duplex links, C.ACM 12, 260 (1969).

[3] Note: In the case of protocol analysis, there are normally only two entities.

[4] Note: The corruption or loss of a message is modeled as a state transition of the $medium$ .

[5] M.G.Gouda, E.G.Manning, Y.T.Yu: On the progress of communication between two finite state machines, doi

[6] P. Zafiropulo, C. West, H. Rudin, D. Cowan, D. Brand : Towards analyzing and synthesizing protocols, IEEE Transactions on Communications ( Volume: 28, Issue: 4, Apr 1980 )

[7] Note: The SAVE construct of SDL can be used to indicate that certain types of messages should not be consumed in the current state, but saved for future processing.

[8] M.F. Al-hammouri and G.v. Bochmann : Realizability of service specifications, Proc. System Analysis and Modelling (SAM) conference 2018, Copenhagen, LNCS, Springer

[9] C. Fournet, T. Hoare, S. K. Rajamani, and J. Rehof : Stuck-free Conformance, Proc. 16th Intl. Conf. on Computer Aided Verification (CAV’04), LNCS, vol. 3114, Springer, 2004

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]