अनुक्रमिक प्रक्रियाओं का संचार करना: Difference between revisions

Revision as of 10:36, 25 May 2023

कंप्यूटर विज्ञान में, अनुक्रमिक प्रक्रियाओं (सीएसपी) को संप्रेषित करना समवर्ती प्रणालियों में परस्पर क्रिया के प्रतिरूप का वर्णन करने के लिए औपचारिक भाषा है ।^[1] यह समवर्ती के गणितीय सिद्धांतों के वर्ग का सदस्य है जिसे चैनल (प्रोग्रामिंग) के माध्यम से निकलने वाले संदेश के आधार पर प्रक्रिया बीजगणित, या प्रक्रिया कलन के रूप में जाना जाता है । सीएसपी ओकैम (प्रोग्रामिंग भाषा) प्रोग्रामिंग भाषा के रचना में अत्यधिक प्रभावशाली था ^[1]^[2] और लिंबो (प्रोग्रामिंग भाषा) जैसी प्रोग्रामिंग भाषाओं के रचना को भी प्रभावित किया था ^[3] राफ्टलिब, एरलांग (प्रोग्रामिंग भाषा),^[4] जाओ (प्रोग्रामिंग भाषा),^[5]^[3] क्रिस्टल (प्रोग्रामिंग भाषा), और क्लोजर का कोर एसिंक्रोनस है।^[6]

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

इतिहास

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

COPY = *[c:character; west?c → east!c]

नामित प्रक्रिया से बार-बार west अक्षर प्राप्त करता है और उस अक्षर को east नाम की प्रक्रिया के समानांतर रचना में भेजता है।

[west::DISASSEMBLE || X::COPY || east::ASSEMBLE]

DISASSEMBLE प्रक्रिया के west में नाम निर्दिष्ट करता है। X COPY प्रक्रिया को और east में ASSEMBLE प्रक्रिया को और इन तीन प्रक्रियाओं को समवर्ती रूप से निष्पादित करता है।^[7]

सीएसपी के मूल संस्करण के प्रकाशन के बाद होरे, स्टीफन ब्रूक्स और बिल रोसको|ए. डब्ल्यू रोस्को ने सीएसपी के सिद्धांत को अपने आधुनिक, प्रक्रिया बीजगणितीय रूप में विकसित और परिष्कृत किया। सीएसपी को प्रक्रिया बीजगणित में विकसित करने के लिए लिया गया दृष्टिकोण रॉबिन मिलनर के कम्युनिकेटिंग सिस्टम्स (सीसीएस) के कलन पर काम से प्रभावित था और इसके विपरीत सीएसपी का सैद्धांतिक संस्करण प्रारंभ में ब्रुक्स, होरे और रोसको द्वारा 1984 के लेख में प्रस्तुत किया गया था,^[14] और बाद में होरे की पुस्तक संचार अनुक्रमिक प्रक्रियाओं में,^[12] जिसे 1985 में प्रकाशित किया गया था। सितंबर 2006 में, वह पुस्तक अभी भी तीसरा सबसे उद्धृत साइटसीर के अनुसार अब तक का कंप्यूटर विज्ञान संदर्भ था (यद्यपि इसके नमूने की प्रकृति के कारण अविश्वसनीय स्रोत)। होरे की किताब के प्रकाशन के बाद से सीएसपी के सिद्धांत में कुछ छोटे बदलाव हुए हैं। इनमें से अधिकांश परिवर्तन सीएसपी प्रक्रिया विश्लेषण और सत्यापन के लिए स्वचालित उपकरणों के आगमन से प्रेरित थे। रोसको का सिद्धांत और समवर्ती का अभ्यास ^[1] सीएसपी के इस नए संस्करण का वर्णन करता है।

अनुप्रयोग

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

सॉफ्टवेयर रचना के लिए सीएसपी के औद्योगिक अनुप्रयोग ने सामान्यतः विश्वास और सुरक्षा-महत्वपूर्ण प्रणालियों पर ध्यान केंद्रित किया है। उदाहरण के लिए, ब्रेमेन इंस्टीट्यूट फॉर सेफ सिस्टम्स और डेमलर क्रिसलर एयरोस्पेस ने फॉल्ट-मैनेजमेंट प्रणाली और एवियोनिक्स इंटरफ़ेस (कोड की लगभग 23,000 लाइनों से मिलकर) को सीएसपी में अंतर्राष्ट्रीय अंतरिक्ष स्टेशन पर उपयोग के लिए तैयार किया और मॉडल का विश्लेषण किया। यह पुष्टि करने के लिए कि उनका रचना डेडलॉक और लाइवलॉक से मुक्त था।^[15]^[16] मॉडलिंग और विश्लेषण प्रक्रिया ऐसी कई त्रुटियों को उजागर करने में सक्षम थी। जिनका अकेले परीक्षण का उपयोग करके पता लगाना कठिन होता है। इसी तरह, प्रैक्सिस हाई इंटीग्रिटी सिस्टम्स ने सुरक्षित स्मार्ट-कार्ड प्रमाणन प्राधिकरण के लिए सॉफ्टवेयर के विकास (कोड की लगभग 100,000 लाइनें) के समय सीएसपी मॉडलिंग और विश्लेषण प्रयुक्त किया जिससे यह सत्यापित किया जा सके कि उनका रचना सुरक्षित और डेडलॉक से मुक्त था। प्रैक्सिस का प्रमाणित है कि तुलनीय प्रणालियों की तुलना में प्रणाली में बहुत कम दोष दर है।^[10]

चूंकि सीएसपी जटिल संदेश एक्सचेंजों को सम्मिलित करने वाली प्रणालियों के मॉडलिंग और विश्लेषण के लिए उपयुक्त है। इसलिए इसे संचार और सुरक्षा प्रोटोकॉल के सत्यापन के लिए भी प्रयुक्त किया गया है। इस प्रकार के अनुप्रयोग का प्रमुख उदाहरण लोवे द्वारा सीएसपी और एफडीआर2 शोधन-परीक्षक का उपयोग नीडम-श्रोएडर प्रोटोकॉल प्रमाणीकरण प्रोटोकॉल पर पहले अज्ञात हमले की खोज करने के लिए और फिर सही प्रोटोकॉल विकसित करने के लिए किया जाता है। आक्रमण को परास्त करने में सक्षम है।^[17]

अनौपचारिक विवरण

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

प्राचीन

सीएसपी अपनी प्रक्रिया बीजगणित में प्राचीन के दो वर्ग प्रदान करता है।

कार्य: घटनाएँ संचार या परस्पर क्रिया का प्रतिनिधित्व करती हैं। उन्हें अविभाज्य और तात्कालिक माना जाता है। वे परमाणु नाम (जैसे चालू, बंद), यौगिक नाम (जैसे वाल्व.ओपन, वाल्व.क्लोज़), या इनपुट/आउटपुट इवेंट (जैसे माउस एक्सवाई, स्क्रीन!बिटमैप) हो सकते हैं।

प्राचीन प्रक्रियाएं

प्राचीन प्रक्रियाएं मौलिक व्यवहारों का प्रतिनिधित्व करती हैं। उदाहरणों में विराम (वह प्रक्रिया जो कुछ भी संचार नहीं करती है, जिसे गतिरोध भी कहा जाता है), और छोडना (जो सफल समाप्ति का प्रतिनिधित्व करता है) सम्मिलित हैं।

बीजगणितीय संचालक

सीएसपी में बीजगणितीय संचालको की विस्तृत श्रृंखला है। प्रमुख हैं:

उपसर्ग: उपसर्ग संचालक नई प्रक्रिया का उत्पादन करने के लिए घटना और प्रक्रिया को जोड़ता है। उदाहरण के लिए, $a\to P$ वह प्रक्रिया है जो $a$ अपने पर्यावरण के साथ संचार करने को तैयार है और उसके बाद $a$ , प्रक्रिया $P$ की तरह व्यवहार करता है .
निर्धारक विकल्प: नियतात्मक (या बाहरी) विकल्प संचालक प्रक्रिया के भविष्य के विकास को दो घटक प्रक्रियाओं के बीच एक विकल्प के रूप में परिभाषित करने की अनुमति देता है और पर्यावरण को किसी प्रक्रिया के लिए प्रारंभिक घटना को संप्रेषित करके विकल्प को हल करने की अनुमति देता है। उदाहरण के लिए, $(a\to P)\Box (b\to Q)$ वह प्रक्रिया है जो प्रारंभिक घटनाओं $a$ और $b$ को संप्रेषित करने के लिए तैयार है और बाद में या तो $P$ या $Q$ ,के रूप व्यवहार करता है जिसके आधार पर पर्यावरण संचार करने के लिए प्रारंभिक घटना का चयन करता है। यदि दोनों $a$ और $b$ को एक साथ संप्रेषित किया गया था, तो विकल्प को गैर-निर्धारित रूप से हल किया जाएगा।
गैर नियतात्मक विकल्प: गैर नियतात्मक (या आंतरिक) विकल्प संचालक प्रक्रिया के भविष्य के विकास को दो घटक प्रक्रियाओं के बीच विकल्प के रूप में परिभाषित करने की अनुमति देता है, किन्तु पर्यावरण को किसी भी नियंत्रण की अनुमति नहीं देता है कि कौन से घटक प्रक्रियाओं का चयन किया जाएगा। उदाहरण के लिए, $(a\to P)\sqcap (b\to Q)$ जैसा व्यवहार कर सकता है $(a\to P)$ या $(b\to Q)$ . मानने से इंकार कर सकता है $a$ या $b$ और संचार करने के लिए तभी बाध्य है जब पर्यावरण दोनों प्रदान करता है $a$ और $b$ . यदि विकल्प के दोनों पक्षों की प्रारंभिक घटनाएँ समान हैं, तो गैर-नियतात्मकता को अनजाने में नाममात्र निर्धारक विकल्प में प्रस्तुत किया जा सकता है। तो, उदाहरण के लिए,; या तो $(a\to P)$ या $(b\to Q)$ की तरह व्यवहार कर सकता है। यह $a$ या $b$ को स्वीकार करने से इंकार कर सकता है और केवल तभी संचार करने के लिए बाध्य होता है। जब पर्यावरण $a$ और $b$ दोनों प्रदान करता है। यदि विकल्प के दोनों पक्षों की प्रारंभिक घटनाएँ समान हैं, तो गैर-नियतात्मकता को अनजाने में एक नाममात्र नियतात्मक विकल्प में प्रस्तुत किया जा सकता है। तो उदाहरण के लिए $(a\to a\to {\text{STOP}})\Box (a\to b\to {\text{STOP}})$ के समान है। $a\to {\big (}(a\to {\text{STOP}})\sqcap (b\to {\text{STOP}}){\big )}$
इंटरलिविंग: इंटरलीविंग संचालक पूरी तरह से स्वतंत्र समवर्ती गतिविधि का प्रतिनिधित्व करता है। प्रक्रिया $P\;|||\;Q$ दोनों के रूप में व्यवहार करता है $P$ और $Q$ इसके साथ ही। दोनों प्रक्रियाओं की घटनाओं को इच्छानुसार समय के साथ जोड़ा जाता है।
इंटरफ़ेस समानांतर: इंटरफ़ेस समानांतर संचालक समवर्ती गतिविधि का प्रतिनिधित्व करता है जिसके लिए घटक प्रक्रियाओं के बीच सिंक्रनाइज़ेशन की आवश्यकता होती है: इंटरफ़ेस समुच्चय में कोई भी घटना तभी हो सकती है जब सभी घटक प्रक्रियाएँ उस घटना में संलग्न होने में सक्षम हों। उदाहरण के लिए, प्रक्रिया $P\;|[\{a\}]|\;Q$ $P$ और $Q$ दोनों की तरह एक साथ व्यवहार करता है। दोनों प्रक्रियाओं $a$ की घटनाओं को इच्छानुसार समय के साथ जोड़ा जाता है। $(a\to P)\;|[\{a\}]|\;(a\to Q)$ कार्य $a$ में सम्मिलित हो सकते हैं और प्रक्रिया बन सकते हैं। $P\;|[\{a\}]|\;Q$ जबकि $(a\to P)\;|[\{a,b\}]|\;(b\to Q)$ बस गतिरोध होगा।
प्रच्छादन: प्रच्छादन वाला संचालक कुछ घटनाओं को अप्राप्य बनाकर सार प्रक्रियाओं की विधि प्रदान करता है। प्रच्छादन का सामान्य उदाहरण है। $(a\to P)\setminus \{a\}$ जो यह मानते हुए कि $P$ में प्रकट नहीं होने वाली घटना $a$ को कम कर देता है। $P$

उदाहरण

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

\mathrm {VendingMachine} =\mathrm {coin} \rightarrow \mathrm {choc} \rightarrow \mathrm {STOP}

एक व्यक्ति जो भुगतान करने के लिए सिक्के या कार्ड का उपयोग करना चुन सकता है। उसे इस प्रकार मॉडल किया जा सकता है।

\mathrm {Person} =(\mathrm {coin} \rightarrow \mathrm {STOP} )\Box (\mathrm {card} \rightarrow \mathrm {STOP} )

इन दोनों प्रक्रियाओं को समानांतर में रखा जा सकता है। जिससे वे दूसरे के साथ परस्पर क्रिया कर सकें। समग्र प्रक्रिया का व्यवहार उन घटनाओं पर निर्भर करता है। जिन पर दो घटक प्रक्रियाओं को सिंक्रनाइज़ करना चाहिए। इस प्रकार,

\mathrm {VendingMachine} \left\vert \left[\left\{\mathrm {coin} ,\mathrm {card} \right\}\right]\right\vert \mathrm {Person} \equiv \mathrm {coin} \rightarrow \mathrm {choc} \rightarrow \mathrm {STOP}

जबकि यदि केवल "कॉइन" पर सिंक्रोनाइज़ेशन की आवश्यकता होती है, तो हम प्राप्त करेंगे

\mathrm {VendingMachine} \left\vert \left[\left\{\mathrm {coin} \right\}\right]\right\vert \mathrm {Person} \equiv \left(\mathrm {coin} \rightarrow \mathrm {choc} \rightarrow \mathrm {STOP} \right)\Box \left(\mathrm {card} \rightarrow \mathrm {STOP} \right)

यदि हम "सिक्का" और "कार्ड" घटनाओं को छिपाकर इस बाद की समग्र प्रक्रिया को सार करते हैं, अर्थात

\left(\left(\mathrm {coin} \rightarrow \mathrm {choc} \rightarrow \mathrm {STOP} \right)\Box \left(\mathrm {card} \rightarrow \mathrm {STOP} \right)\right)\setminus \left\{\mathrm {coin,card} \right\}

हमें गैर-नियतात्मक प्रक्रिया मिलती है।

\left(\mathrm {choc} \rightarrow \mathrm {STOP} \right)\sqcap \mathrm {STOP}

यह ऐसी प्रक्रिया है जो या तो "चोक" घटना की प्रस्तुति करती है और फिर रुक जाती है, या बस रुक जाती है। दूसरे शब्दों में, यदि हम अमूर्तता को प्रणाली के बाहरी दृश्य के रूप में मानते हैं (उदाहरण के लिए, कोई व्यक्ति जो व्यक्ति द्वारा किए गए निर्णय को नहीं देखता है), गैर-नियतात्मक एल्गोरिदम प्रस्तुत किया गया है।

औपचारिक परिभाषा

वाक्य - विन्यास

सीएसपी का वाक्य - विन्यास "नियमबद्ध" विधियों को परिभाषित करता है। जिसमें प्रक्रियाओं और घटनाओं को जोड़ा जा सकता है। माना $e$ एक घटना हो, और $X$ घटनाओं का समुच्चय हो। तब सीएसपी के मूल वाक्य - विन्यास को इस प्रकार परिभाषित किया जा सकता है।

\mathbf {div}

[roscoe-1] 1.0 ^1.1 ^1.2 ^1.3 Roscoe, A. W. (1997). समरूपता का सिद्धांत और अभ्यास (PDF). Prentice Hall. ISBN 978-0-13-674409-2.

[2] Inmos (1995-05-12). occam 2.1 Reference Manual (PDF). SGS-THOMSON Microelectronics Ltd., INMOS document 72 occ 45 03.

[cox-3] 3.0 ^3.1 Cox, Russ. "बेल लैब्स और सीएसपी थ्रेड्स". Retrieved 2010-04-15.

[4] "10 अकादमिक और ऐतिहासिक प्रश्न". Retrieved 2021-11-15.

[golang-5] "FAQ: Why build concurrency on the ideas of CSP?". The Go Programming Language. Retrieved 2021-10-15.

[clojure-core-async-6] Hickey, Rich (2013-06-28). "क्लोजर कोर.एसिंक चैनल". Retrieved 2021-10-15.

[hoare1978-7] 7.0 ^7.1 Hoare, C. A. R. (1978). "Communicating sequential processes". Communications of the ACM. 21 (8): 666–677. doi:10.1145/359576.359585. S2CID 849342.

[25years-8] Abdallah, Ali E.; Jones, Cliff B.; Sanders, Jeff W. (2005). Communicating Sequential Processes: The First 25 Years. LNCS. Vol. 3525. Springer. ISBN 9783540258131.

[barrett-9] 9.0 ^9.1 Barrett, G. (1995). "Model checking in practice: The T9000 Virtual Channel Processor". IEEE Transactions on Software Engineering. 21 (2): 69–78. doi:10.1109/32.345823.

[hall-10] 10.0 ^10.1 Hall, A; Chapman, R. (2002). "Correctness by construction: Developing a commercial secure system" (PDF). IEEE Software. 19 (1): 18–25. CiteSeerX 10.1.1.16.1811. doi:10.1109/52.976937.

[11] Creese, S. (2001). Data Independent Induction: CSP Model Checking of Arbitrary Sized Networks (D. Phil.). Oxford University. CiteSeerX 10.1.1.13.7185.

[hoare-12] 12.0 ^12.1 Hoare, C. A. R. (1985). अनुक्रमिक प्रक्रियाओं का संचार करना. Prentice Hall. ISBN 978-0-13-153289-2.

[clinger1981-13] Clinger, William (June 1981). अभिनेता शब्दार्थ की नींव (Mathematics Doctoral Dissertation). MIT. hdl:1721.1/6935.

[14] Brookes, Stephen; Hoare, C. A. R.; Roscoe, A. W. (1984). "अनुक्रमिक प्रक्रियाओं के संचार का सिद्धांत". Journal of the ACM. 31 (3): 560–599. doi:10.1145/828.833. S2CID 488666.

[15] Buth, B.; M. Kouvaras; J. Peleska; H. Shi (December 1997). "दोष-सहिष्णु प्रणाली के लिए गतिरोध विश्लेषण". Proceedings of the 6th International Conference on Algebraic Methodology and Software Technology (AMAST’97). pp. 60–75.

[16] Buth, B.; J. Peleska; H. Shi (January 1999). "दोष-सहिष्णु प्रणाली के लाइवलॉक विश्लेषण के लिए विधियों का संयोजन". Proceedings of the 7th International Conference on Algebraic Methodology and Software Technology (AMAST’98). pp. 124–139.

[17] Lowe, G. (1996). "Breaking and fixing the Needham–Schroeder public-key protocol using FDR". Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer-Verlag. pp. 147–166.

[18] Scattergood, J.B. (1998). "मशीन-पठनीय सीएसपी का शब्दार्थ और कार्यान्वयन". D.Phil. Oxford University Computing Laboratory. {{cite journal}}: Cite journal requires |journal= (help)

[19] A.W. Roscoe (1994). "मॉडल-चेकिंग सीएसपी". In A Classical Mind: essays in Honour of C.A.R. Hoare. Prentice Hall. {{cite journal}}: Cite journal requires |journal= (help)

[20] "Introduction — FDR 4.2.4 documentation". www.cs.ox.ac.uk.

[21] Parashkevov, Atanas N.; Yantchev, Jay (1996). "ARC – a tool for efficient refinement and equivalence checking for CSP". IEEE Int. Conf. on Algorithms and Architectures for Parallel Processing ICA3PP '96. pp. 68–75. CiteSeerX 10.1.1.45.3212.

[22] Leuschel, Michael; Fontaine, Marc (2008). "Probing the Depths of CSP-M: A new FDR-compliant Validation Tool" (PDF). ICFEM 2008. Springer-Verlag. Archived from the original (PDF) on 2011-07-19. Retrieved 2008-11-26.

[23] Sun, Jun; Liu, Yang; Dong, Jin Song (2009). "PAT: Towards Flexible Verification under Fairness" (PDF). Proceedings of the 20th International Conference on Computer-Aided Verification (CAV 2009). Lecture Notes in Computer Science. Vol. 5643. Springer. Archived from the original (PDF) on 2011-06-11. Retrieved 2009-06-16.

[24] Sun, Jun; Liu, Yang; Dong, Jin Song (2008). "Model Checking CSP Revisited: Introducing a Process Analysis Toolkit" (PDF). Proceedings of the Third International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2008). Communications in Computer and Information Science. Vol. 17. Springer. pp. 307–322. Archived from the original (PDF) on 2009-01-08. Retrieved 2009-01-15.

[25] Sun, Jun; Liu, Yang; Dong, Jin Song; Chen, Chunqing (2009). "सिस्टम विशिष्टता और सत्यापन के लिए विनिर्देशों और कार्यक्रमों को एकीकृत करना" (PDF). IEEE Int. Conf. on Theoretical Aspects of Software Engineering TASE '09. Archived from the original (PDF) on 2011-06-11. Retrieved 2009-04-13.

[26] Green, Mark; Abdallah, Ali (2002). "संचार प्रणालियों के अनुकूलन के लिए प्रदर्शन विश्लेषण और व्यवहार ट्यूनिंग". Communicating Process Architectures 2002.

[27] Brooke, Phillip; Paige, Richard (2007). "सीएसपीसिम के साथ आलसी अन्वेषण और सीएसपी मॉडल की जांच". Communicating Process Architectures 2007.

[28] ISO 8807, Language of Temporal Ordering Specification

[29] Geraint Jones (1990). "Sharp as a Razor: A Queen's Award for the Computing Laboratory". The Oxford Magazine (59, Fourth Week, Trinity Term).

[30] Len Shustek (March 2009). "C.A.R के साथ एक साक्षात्कार होरे". Communications of the ACM. 52 (3): 38–41. doi:10.1145/1467247.1467261. S2CID 1868477.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]

[19]

[20]

[21]

[22]

[23]

[24]

[25]

[26]

[27]

[28]

[29]

[30]

Anonymous

Search

अनुक्रमिक प्रक्रियाओं का संचार करना: Difference between revisions

Namespaces

More

Page actions

Revision as of 10:36, 25 May 2023

Contents