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

Revision as of 11:35, 22 May 2023

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

इतिहास

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

कॉपी = * [सी: चरित्र; पश्चिम?सी → पूर्व!सी]

नामित प्रक्रिया से बार-बार चरित्र प्राप्त करता है west और उस कैरेक्टर को नाम प्रोसेस करने के लिए भेजता है east. समानांतर रचना

[पश्चिम::अलग करना || एक्स :: कॉपी || पूर्व :: इकट्ठा]

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

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

अनुप्रयोग

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

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

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

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

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

आदिम

CSP अपनी प्रक्रिया बीजगणित में प्रिमिटिव के दो वर्ग प्रदान करता है:

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

आदिम प्रक्रियाएं

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

बीजगणितीय ऑपरेटर

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

उपसर्ग: उपसर्ग ऑपरेटर नई प्रक्रिया का उत्पादन करने के लिए घटना और प्रक्रिया को जोड़ता है। उदाहरण के लिए, $a\to P$ वह प्रक्रिया है जो संवाद करने को तैयार है $a$ अपने पर्यावरण के साथ और उसके बाद $a$ , प्रक्रिया की तरह व्यवहार करता है $P$ .
नियतात्मक पसंद: नियतात्मक (या बाहरी) पसंद ऑपरेटर प्रक्रिया के भविष्य के विकास को दो घटक प्रक्रियाओं के बीच एक विकल्प के रूप में परिभाषित करने की अनुमति देता है और पर्यावरण को किसी प्रक्रिया के लिए प्रारंभिक घटना को संप्रेषित करके पसंद को हल करने की अनुमति देता है। उदाहरण के लिए, $(a\to P)\Box (b\to Q)$ वह प्रक्रिया है जो प्रारंभिक घटनाओं को संप्रेषित करने के लिए तैयार है $a$ और $b$ और बाद में या तो व्यवहार करता है $P$ या $Q$ , पर्यावरण किस प्रारंभिक घटना के आधार पर संवाद करना चुनता है। अगर दोनों $a$ और $b$ को एक साथ संप्रेषित किया गया था, तो विकल्प को गैर-निर्धारित रूप से हल किया जाएगा।
गैर नियतात्मक विकल्प: nondeterministic (या आंतरिक) पसंद ऑपरेटर प्रक्रिया के भविष्य के विकास को दो घटक प्रक्रियाओं के बीच विकल्प के रूप में परिभाषित करने की अनुमति देता है, लेकिन पर्यावरण को किसी भी नियंत्रण की अनुमति नहीं देता है कि कौन से घटक प्रक्रियाओं का चयन किया जाएगा। उदाहरण के लिए, $(a\to P)\sqcap (b\to Q)$ जैसा व्यवहार कर सकता है $(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\}$ जो, यह मानते हुए कि घटना $a$ में दिखाई नहीं देता $P$ , बस इतना कम कर देता है $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}

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

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

सिंटेक्स

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

\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]

@@ Line 1: / Line 1: @@
 {{Short description|Formal model in concurrency theory}}
 {{distinguish|Constraint satisfaction problem}}
-[[कंप्यूटर विज्ञान]] में, अनुक्रमिक प्रक्रियाओं (सीएसपी) को संप्रेषित करना समवर्ती प्रणालियों में बातचीत के [[ नमूना ]] का वर्णन करने के लिए एक [[औपचारिक भाषा]] है।<ref name="roscoe">{{cite book |first=A. W. |last=Roscoe |author-link=Bill Roscoe |title=समरूपता का सिद्धांत और अभ्यास|publisher=[[Prentice Hall]] |isbn=978-0-13-674409-2 |year=1997 |url-access=registration |url=http://www.cs.ox.ac.uk/bill.roscoe/publications/68b.pdf}}</ref> यह [[चैनल (प्रोग्रामिंग)]] के माध्यम से गुजरने वाले संदेश के आधार पर प्रक्रिया बीजगणित, या प्रक्रिया कलन के रूप में ज्ञात संगामिति के गणितीय सिद्धांतों के परिवार का एक सदस्य है। सीएसपी [[ओकैम (प्रोग्रामिंग भाषा)]] प्रोग्रामिंग भाषा के डिजाइन में अत्यधिक प्रभावशाली था<ref name="roscoe" /><ref>{{cite book |author=Inmos |author-link=Inmos |url=http://www.wotug.org/occam/documentation/oc21refman.pdf |title=occam 2.1 Reference Manual |publisher=SGS-THOMSON Microelectronics Ltd. |date=1995-05-12}}, INMOS document 72 occ 45 03.</ref> और लिंबो (प्रोग्रामिंग भाषा) जैसी प्रोग्रामिंग भाषाओं के डिजाइन को भी प्रभावित किया,<ref name="cox">{{cite web |title=बेल लैब्स और सीएसपी थ्रेड्स|url=http://swtch.com/~rsc/thread/ |first=Russ |last=Cox |access-date=2010-04-15}}</ref> [[राफ्टलिब]], एरलांग (प्रोग्रामिंग भाषा),<ref>{{cite web |title=10 अकादमिक और ऐतिहासिक प्रश्न|url=https://www.erlang.org/faq/academic.html |access-date=2021-11-15}}</ref> [[जाओ (प्रोग्रामिंग भाषा)]],<ref name="golang">{{cite web |title=FAQ: Why build concurrency on the ideas of CSP? |url=http://golang.org/doc/go_faq.html#csp |work=The Go Programming Language |access-date=2021-10-15}}</ref><ref name="cox"/>[[क्रिस्टल (प्रोग्रामिंग भाषा)]], और [[क्लोजर]] का core.async।<ref name="clojure-core-async">{{cite web |title=क्लोजर कोर.एसिंक चैनल|url=https://clojure.org/news/2013/06/28/clojure-clore-async-channels#_history |first=Rich |last=Hickey |date=2013-06-28 |access-date=2021-10-15}}</ref>
+[[कंप्यूटर विज्ञान]] में, अनुक्रमिक प्रक्रियाओं (सीएसपी) को संप्रेषित करना समवर्ती प्रणालियों में बातचीत के [[ नमूना ]] का वर्णन करने के लिए  [[औपचारिक भाषा]] है।<ref name="roscoe">{{cite book |first=A. W. |last=Roscoe |author-link=Bill Roscoe |title=समरूपता का सिद्धांत और अभ्यास|publisher=[[Prentice Hall]] |isbn=978-0-13-674409-2 |year=1997 |url-access=registration |url=http://www.cs.ox.ac.uk/bill.roscoe/publications/68b.pdf}}</ref> यह [[चैनल (प्रोग्रामिंग)]] के माध्यम से गुजरने वाले संदेश के आधार पर प्रक्रिया बीजगणित, या प्रक्रिया कलन के रूप में ज्ञात संगामिति के गणितीय सिद्धांतों के परिवार का  सदस्य है। सीएसपी [[ओकैम (प्रोग्रामिंग भाषा)]] प्रोग्रामिंग भाषा के डिजाइन में अत्यधिक प्रभावशाली था<ref name="roscoe" /><ref>{{cite book |author=Inmos |author-link=Inmos |url=http://www.wotug.org/occam/documentation/oc21refman.pdf |title=occam 2.1 Reference Manual |publisher=SGS-THOMSON Microelectronics Ltd. |date=1995-05-12}}, INMOS document 72 occ 45 03.</ref> और लिंबो (प्रोग्रामिंग भाषा) जैसी प्रोग्रामिंग भाषाओं के डिजाइन को भी प्रभावित किया,<ref name="cox">{{cite web |title=बेल लैब्स और सीएसपी थ्रेड्स|url=http://swtch.com/~rsc/thread/ |first=Russ |last=Cox |access-date=2010-04-15}}</ref> [[राफ्टलिब]], एरलांग (प्रोग्रामिंग भाषा),<ref>{{cite web |title=10 अकादमिक और ऐतिहासिक प्रश्न|url=https://www.erlang.org/faq/academic.html |access-date=2021-11-15}}</ref> [[जाओ (प्रोग्रामिंग भाषा)]],<ref name="golang">{{cite web |title=FAQ: Why build concurrency on the ideas of CSP? |url=http://golang.org/doc/go_faq.html#csp |work=The Go Programming Language |access-date=2021-10-15}}</ref><ref name="cox"/>[[क्रिस्टल (प्रोग्रामिंग भाषा)]], और [[क्लोजर]] का core.async।<ref name="clojure-core-async">{{cite web |title=क्लोजर कोर.एसिंक चैनल|url=https://clojure.org/news/2013/06/28/clojure-clore-async-channels#_history |first=Rich |last=Hickey |date=2013-06-28 |access-date=2021-10-15}}</ref>
-सीएसपी को पहली बार 1978 में [[टोनी होरे]] के एक लेख में वर्णित किया गया था,<ref name="hoare1978">{{cite journal
+सीएसपी को पहली बार 1978 में [[टोनी होरे]] के  लेख में वर्णित किया गया था,<ref name="hoare1978">{{cite journal
 |last=Hoare
 |first=C. A. R.
@@ Line 30: / Line 30: @@
 |pages=69–78
 |year=1995
-|doi=10.1109/32.345823}}</ref> साथ ही एक सुरक्षित ईकॉमर्स सिस्टम।<ref name="hall">{{cite journal
+|doi=10.1109/32.345823}}</ref> साथ ही  सुरक्षित ईकॉमर्स सिस्टम।<ref name="hall">{{cite journal
 |last1 = Hall
 |first1=A
@@ Line 48: / Line 48: @@
 == इतिहास ==
-होरे के मूल 1978 के लेख में प्रस्तुत सीएसपी का संस्करण अनिवार्य रूप से एक प्रक्रिया कलन के बजाय एक समवर्ती प्रोग्रामिंग भाषा थी। सीएसपी के बाद के संस्करणों की तुलना में इसमें काफी भिन्न [[ वाक्य - विन्यास ]] था, गणितीय रूप से परिभाषित शब्दार्थ नहीं था,<ref name="hoare">{{cite book |last=Hoare |first=C. A. R. |author-link=C. A. R. Hoare |title=अनुक्रमिक प्रक्रियाओं का संचार करना|publisher=Prentice Hall |isbn=978-0-13-153289-2 |year=1985}}</ref> और अबाधित अनिर्धारणवाद का प्रतिनिधित्व करने में असमर्थ था।<ref name="clinger1981">{{Cite thesis |first = William |last = Clinger |author-link = William Clinger (computer scientist) |title=अभिनेता शब्दार्थ की नींव|publisher=MIT |type=Mathematics Doctoral Dissertation |date=June 1981 |hdl = 1721.1/6935 }}</ref> मूल सीएसपी में प्रोग्राम एक निश्चित संख्या में अनुक्रमिक प्रक्रियाओं की एक समानांतर रचना के रूप में लिखे गए थे जो एक दूसरे के साथ सख्ती से सिंक्रोनस मैसेज-पासिंग के माध्यम से संचार करते थे। सीएसपी के बाद के संस्करणों के विपरीत, प्रत्येक प्रक्रिया को एक स्पष्ट नाम दिया गया था, और संदेश के स्रोत या गंतव्य को भेजने या प्राप्त करने की प्रक्रिया के नाम को निर्दिष्ट करके परिभाषित किया गया था। उदाहरण के लिए, प्रक्रिया
+होरे के मूल 1978 के लेख में प्रस्तुत सीएसपी का संस्करण अनिवार्य रूप से  प्रक्रिया कलन के बजाय  समवर्ती प्रोग्रामिंग भाषा थी। सीएसपी के बाद के संस्करणों की तुलना में इसमें काफी भिन्न [[ वाक्य - विन्यास ]] था, गणितीय रूप से परिभाषित शब्दार्थ नहीं था,<ref name="hoare">{{cite book |last=Hoare |first=C. A. R. |author-link=C. A. R. Hoare |title=अनुक्रमिक प्रक्रियाओं का संचार करना|publisher=Prentice Hall |isbn=978-0-13-153289-2 |year=1985}}</ref> और अबाधित अनिर्धारणवाद का प्रतिनिधित्व करने में असमर्थ था।<ref name="clinger1981">{{Cite thesis |first = William |last = Clinger |author-link = William Clinger (computer scientist) |title=अभिनेता शब्दार्थ की नींव|publisher=MIT |type=Mathematics Doctoral Dissertation |date=June 1981 |hdl = 1721.1/6935 }}</ref> मूल सीएसपी में प्रोग्राम  निश्चित संख्या में अनुक्रमिक प्रक्रियाओं की  समानांतर रचना के रूप में लिखे गए थे जो एक दूसरे के साथ सख्ती से सिंक्रोनस मैसेज-पासिंग के माध्यम से संचार करते थे। सीएसपी के बाद के संस्करणों के विपरीत, प्रत्येक प्रक्रिया को  स्पष्ट नाम दिया गया था, और संदेश के स्रोत या गंतव्य को भेजने या प्राप्त करने की प्रक्रिया के नाम को निर्दिष्ट करके परिभाषित किया गया था। उदाहरण के लिए, प्रक्रिया
   कॉपी = * [सी: चरित्र; पश्चिम?सी → पूर्व!सी]
-नामित प्रक्रिया से बार-बार एक चरित्र प्राप्त करता है <code>west</code> और उस कैरेक्टर को नाम प्रोसेस करने के लिए भेजता है <code>east</code>. समानांतर रचना
+नामित प्रक्रिया से बार-बार  चरित्र प्राप्त करता है <code>west</code> और उस कैरेक्टर को नाम प्रोसेस करने के लिए भेजता है <code>east</code>. समानांतर रचना
   [पश्चिम::अलग करना || एक्स :: कॉपी || पूर्व :: इकट्ठा]
@@ Line 58: / Line 58: @@
 नाम देता है <code>west</code> तक <code>DISASSEMBLE</code> प्रक्रिया, <code>X</code> तक <code>COPY</code> प्रक्रिया, और <code>east</code> तक <code>ASSEMBLE</code> प्रक्रिया, और इन तीन प्रक्रियाओं को समवर्ती रूप से निष्पादित करता है।<ref name="hoare1978" />
-सीएसपी के मूल संस्करण के प्रकाशन के बाद होरे, स्टीफन ब्रूक्स और बिल रोसको|ए. डब्ल्यू। रोस्को ने सीएसपी के सिद्धांत को अपने आधुनिक, प्रक्रिया बीजगणितीय रूप में विकसित और परिष्कृत किया। CSP को एक प्रक्रिया बीजगणित में विकसित करने के लिए लिया गया दृष्टिकोण [[रॉबिन मिलनर]] के कम्युनिकेटिंग सिस्टम्स (CCS) के कलन पर काम से प्रभावित था और इसके विपरीत। सीएसपी का सैद्धांतिक संस्करण शुरू में ब्रुक्स, होरे और रोसको द्वारा 1984 के एक लेख में प्रस्तुत किया गया था,<ref>{{cite journal |first1=Stephen |last1=Brookes |author2-link = C. A. R. Hoare |first2 = C. A. R. |last2 = Hoare |author3-link = Bill Roscoe |author3-first = A. W. |author3-last = Roscoe |title = अनुक्रमिक प्रक्रियाओं के संचार का सिद्धांत|journal=[[Journal of the ACM]] |volume=31 |issue=3 |pages=560–599 |year=1984 |doi=10.1145/828.833|s2cid=488666 |doi-access=free }}</ref> और बाद में होरे की पुस्तक संचार अनुक्रमिक प्रक्रियाओं में,<ref name="hoare" />जिसे 1985 में प्रकाशित किया गया था। सितंबर 2006 में, वह पुस्तक अभी भी [http://citeseer.ist.psu.edu/articles.html तीसरा सबसे उद्धृत] [[Citeseer]] के अनुसार अब तक का कंप्यूटर विज्ञान संदर्भ था (यद्यपि इसके नमूने की प्रकृति के कारण एक अविश्वसनीय स्रोत)। होरे की किताब के प्रकाशन के बाद से सीएसपी के सिद्धांत में कुछ छोटे बदलाव हुए हैं। इनमें से अधिकांश परिवर्तन CSP प्रक्रिया विश्लेषण और सत्यापन के लिए स्वचालित उपकरणों के आगमन से प्रेरित थे। रोसको का सिद्धांत और संगामिति का अभ्यास<ref name="roscoe" />CSP के इस नए संस्करण का वर्णन करता है।
+सीएसपी के मूल संस्करण के प्रकाशन के बाद होरे, स्टीफन ब्रूक्स और बिल रोसको|ए. डब्ल्यू। रोस्को ने सीएसपी के सिद्धांत को अपने आधुनिक, प्रक्रिया बीजगणितीय रूप में विकसित और परिष्कृत किया। CSP को  प्रक्रिया बीजगणित में विकसित करने के लिए लिया गया दृष्टिकोण [[रॉबिन मिलनर]] के कम्युनिकेटिंग सिस्टम्स (CCS) के कलन पर काम से प्रभावित था और इसके विपरीत। सीएसपी का सैद्धांतिक संस्करण शुरू में ब्रुक्स, होरे और रोसको द्वारा 1984 के  लेख में प्रस्तुत किया गया था,<ref>{{cite journal |first1=Stephen |last1=Brookes |author2-link = C. A. R. Hoare |first2 = C. A. R. |last2 = Hoare |author3-link = Bill Roscoe |author3-first = A. W. |author3-last = Roscoe |title = अनुक्रमिक प्रक्रियाओं के संचार का सिद्धांत|journal=[[Journal of the ACM]] |volume=31 |issue=3 |pages=560–599 |year=1984 |doi=10.1145/828.833|s2cid=488666 |doi-access=free }}</ref> और बाद में होरे की पुस्तक संचार अनुक्रमिक प्रक्रियाओं में,<ref name="hoare" />जिसे 1985 में प्रकाशित किया गया था। सितंबर 2006 में, वह पुस्तक अभी भी [http://citeseer.ist.psu.edu/articles.html तीसरा सबसे उद्धृत] [[Citeseer]] के अनुसार अब तक का कंप्यूटर विज्ञान संदर्भ था (यद्यपि इसके नमूने की प्रकृति के कारण  अविश्वसनीय स्रोत)। होरे की किताब के प्रकाशन के बाद से सीएसपी के सिद्धांत में कुछ छोटे बदलाव हुए हैं। इनमें से अधिकांश परिवर्तन CSP प्रक्रिया विश्लेषण और सत्यापन के लिए स्वचालित उपकरणों के आगमन से प्रेरित थे। रोसको का सिद्धांत और संगामिति का अभ्यास<ref name="roscoe" />CSP के इस नए संस्करण का वर्णन करता है।
 === अनुप्रयोग ===
-सीएसपी का एक प्रारंभिक और महत्वपूर्ण अनुप्रयोग आईएनएमओएस टी9000 ट्रांसप्यूटर के तत्वों के विनिर्देशन और सत्यापन के लिए इसका उपयोग था, एक जटिल सुपरस्केलर पाइपलाइन प्रोसेसर जिसे बड़े पैमाने पर मल्टीप्रोसेसिंग का समर्थन करने के लिए डिज़ाइन किया गया था। सीएसपी को प्रोसेसर पाइपलाइन और वर्चुअल चैनल प्रोसेसर दोनों की शुद्धता की पुष्टि करने के लिए नियोजित किया गया था, जो प्रोसेसर के लिए ऑफ-चिप संचार प्रबंधित करता था।<ref name="barrett" />
+सीएसपी का  प्रारंभिक और महत्वपूर्ण अनुप्रयोग आईएनएमओएस टी9000 ट्रांसप्यूटर के तत्वों के विनिर्देशन और सत्यापन के लिए इसका उपयोग था,  जटिल सुपरस्केलर पाइपलाइन प्रोसेसर जिसे बड़े पैमाने पर मल्टीप्रोसेसिंग का समर्थन करने के लिए डिज़ाइन किया गया था। सीएसपी को प्रोसेसर पाइपलाइन और वर्चुअल चैनल प्रोसेसर दोनों की शुद्धता की पुष्टि करने के लिए नियोजित किया गया था, जो प्रोसेसर के लिए ऑफ-चिप संचार प्रबंधित करता था।<ref name="barrett" />
-सॉफ्टवेयर डिजाइन के लिए सीएसपी के औद्योगिक अनुप्रयोग ने आमतौर पर भरोसेमंद और सुरक्षा-महत्वपूर्ण प्रणालियों पर ध्यान केंद्रित किया है। उदाहरण के लिए, ब्रेमेन इंस्टीट्यूट फॉर सेफ सिस्टम्स और [[डेमलर क्रिसलर एयरोस्पेस]] | डेमलर-बेंज एयरोस्पेस ने एक फॉल्ट-मैनेजमेंट सिस्टम और एवियोनिक्स इंटरफ़ेस (कोड की लगभग 23,000 लाइनों से मिलकर) को सीएसपी में अंतर्राष्ट्रीय अंतरिक्ष स्टेशन पर उपयोग के लिए तैयार किया और मॉडल का विश्लेषण किया। यह पुष्टि करने के लिए कि उनका डिज़ाइन डेडलॉक और लाइवलॉक से मुक्त था।<ref>{{cite conference |first=B. |last=Buth |author2=M. Kouvaras |author3=J. Peleska |author4=H. Shi |title=दोष-सहिष्णु प्रणाली के लिए गतिरोध विश्लेषण|book-title=Proceedings of the 6th International Conference on Algebraic Methodology and Software Technology (AMAST’97) |pages = 60–75 |date=December 1997}}</ref><ref>{{cite conference |first=B. |last=Buth |author2=J. Peleska |author3=H. Shi |title=दोष-सहिष्णु प्रणाली के लाइवलॉक विश्लेषण के लिए विधियों का संयोजन|book-title=Proceedings of the 7th International Conference on Algebraic Methodology and Software Technology (AMAST’98) |pages=124–139 |date=January 1999}}</ref> मॉडलिंग और विश्लेषण प्रक्रिया ऐसी कई त्रुटियों को उजागर करने में सक्षम थी जिनका अकेले परीक्षण का उपयोग करके पता लगाना मुश्किल होता। इसी तरह, [[प्रैक्सिस हाई इंटीग्रिटी सिस्टम्स]] ने एक सुरक्षित स्मार्ट-कार्ड प्रमाणन प्राधिकरण के लिए सॉफ्टवेयर के विकास (कोड की लगभग 100,000 लाइनें) के दौरान सीएसपी मॉडलिंग और विश्लेषण लागू किया ताकि यह सत्यापित किया जा सके कि उनका डिज़ाइन सुरक्षित और डेडलॉक से मुक्त था। प्रैक्सिस का दावा है कि तुलनीय प्रणालियों की तुलना में प्रणाली में बहुत कम दोष दर है।<ref name="hall" />
+सॉफ्टवेयर डिजाइन के लिए सीएसपी के औद्योगिक अनुप्रयोग ने आमतौर पर भरोसेमंद और सुरक्षा-महत्वपूर्ण प्रणालियों पर ध्यान केंद्रित किया है। उदाहरण के लिए, ब्रेमेन इंस्टीट्यूट फॉर सेफ सिस्टम्स और [[डेमलर क्रिसलर एयरोस्पेस]] | डेमलर-बेंज एयरोस्पेस ने  फॉल्ट-मैनेजमेंट सिस्टम और एवियोनिक्स इंटरफ़ेस (कोड की लगभग 23,000 लाइनों से मिलकर) को सीएसपी में अंतर्राष्ट्रीय अंतरिक्ष स्टेशन पर उपयोग के लिए तैयार किया और मॉडल का विश्लेषण किया। यह पुष्टि करने के लिए कि उनका डिज़ाइन डेडलॉक और लाइवलॉक से मुक्त था।<ref>{{cite conference |first=B. |last=Buth |author2=M. Kouvaras |author3=J. Peleska |author4=H. Shi |title=दोष-सहिष्णु प्रणाली के लिए गतिरोध विश्लेषण|book-title=Proceedings of the 6th International Conference on Algebraic Methodology and Software Technology (AMAST’97) |pages = 60–75 |date=December 1997}}</ref><ref>{{cite conference |first=B. |last=Buth |author2=J. Peleska |author3=H. Shi |title=दोष-सहिष्णु प्रणाली के लाइवलॉक विश्लेषण के लिए विधियों का संयोजन|book-title=Proceedings of the 7th International Conference on Algebraic Methodology and Software Technology (AMAST’98) |pages=124–139 |date=January 1999}}</ref> मॉडलिंग और विश्लेषण प्रक्रिया ऐसी कई त्रुटियों को उजागर करने में सक्षम थी जिनका अकेले परीक्षण का उपयोग करके पता लगाना मुश्किल होता। इसी तरह, [[प्रैक्सिस हाई इंटीग्रिटी सिस्टम्स]] ने  सुरक्षित स्मार्ट-कार्ड प्रमाणन प्राधिकरण के लिए सॉफ्टवेयर के विकास (कोड की लगभग 100,000 लाइनें) के दौरान सीएसपी मॉडलिंग और विश्लेषण लागू किया ताकि यह सत्यापित किया जा सके कि उनका डिज़ाइन सुरक्षित और डेडलॉक से मुक्त था। प्रैक्सिस का दावा है कि तुलनीय प्रणालियों की तुलना में प्रणाली में बहुत कम दोष दर है।<ref name="hall" />
-चूंकि सीएसपी जटिल संदेश एक्सचेंजों को शामिल करने वाली प्रणालियों के मॉडलिंग और विश्लेषण के लिए उपयुक्त है, इसलिए इसे संचार और सुरक्षा प्रोटोकॉल के सत्यापन के लिए भी लागू किया गया है। इस प्रकार के अनुप्रयोग का एक प्रमुख उदाहरण लोवे द्वारा CSP और [[FDR2]]|FDR शोधन-परीक्षक का उपयोग नीडम-श्रोएडर प्रोटोकॉल|नीडम-श्रोएडर सार्वजनिक-कुंजी प्रमाणीकरण प्रोटोकॉल पर पहले अज्ञात हमले की खोज करने के लिए और फिर एक सही प्रोटोकॉल विकसित करने के लिए किया जाता है। आक्रमण को परास्त करने में सक्षम है।<ref>{{cite conference |first=G. |last=Lowe |title=Breaking and fixing the Needham–Schroeder public-key protocol using FDR |book-title=Tools and Algorithms for the Construction and Analysis of Systems (TACAS) |pages=147–166 |publisher=Springer-Verlag |year=1996 |url=http://citeseer.ist.psu.edu/lowe96breaking.html}}</ref>
+चूंकि सीएसपी जटिल संदेश एक्सचेंजों को शामिल करने वाली प्रणालियों के मॉडलिंग और विश्लेषण के लिए उपयुक्त है, इसलिए इसे संचार और सुरक्षा प्रोटोकॉल के सत्यापन के लिए भी लागू किया गया है। इस प्रकार के अनुप्रयोग का  प्रमुख उदाहरण लोवे द्वारा CSP और [[FDR2]]|FDR शोधन-परीक्षक का उपयोग नीडम-श्रोएडर प्रोटोकॉल|नीडम-श्रोएडर सार्वजनिक-कुंजी प्रमाणीकरण प्रोटोकॉल पर पहले अज्ञात हमले की खोज करने के लिए और फिर  सही प्रोटोकॉल विकसित करने के लिए किया जाता है। आक्रमण को परास्त करने में सक्षम है।<ref>{{cite conference |first=G. |last=Lowe |title=Breaking and fixing the Needham–Schroeder public-key protocol using FDR |book-title=Tools and Algorithms for the Construction and Analysis of Systems (TACAS) |pages=147–166 |publisher=Springer-Verlag |year=1996 |url=http://citeseer.ist.psu.edu/lowe96breaking.html}}</ref>
 == अनौपचारिक विवरण ==
-जैसा कि इसके नाम से पता चलता है, सीएसपी उन घटक प्रक्रियाओं के संदर्भ में सिस्टम के विवरण की अनुमति देता है जो स्वतंत्र रूप से संचालित होते हैं, और केवल संदेश पासिंग | संदेश-पासिंग संचार के माध्यम से एक दूसरे के साथ बातचीत करते हैं। हालांकि, सीएसपी नाम का अनुक्रमिक हिस्सा अब एक मिथ्या नाम है, क्योंकि आधुनिक सीएसपी घटक प्रक्रियाओं को अनुक्रमिक प्रक्रियाओं के रूप में और अधिक आदिम प्रक्रियाओं की समानांतर संरचना के रूप में परिभाषित करने की अनुमति देता है। विभिन्न प्रक्रियाओं के बीच संबंध, और जिस तरह से प्रत्येक प्रक्रिया अपने पर्यावरण के साथ संचार करती है, उसे विभिन्न [[प्रक्रिया गणना]] ऑपरेटरों का उपयोग करके वर्णित किया गया है। इस बीजगणितीय दृष्टिकोण का उपयोग करते हुए, कुछ आदिम तत्वों से काफी जटिल प्रक्रिया विवरणों का निर्माण आसानी से किया जा सकता है।
+जैसा कि इसके नाम से पता चलता है, सीएसपी उन घटक प्रक्रियाओं के संदर्भ में सिस्टम के विवरण की अनुमति देता है जो स्वतंत्र रूप से संचालित होते हैं, और केवल संदेश पासिंग | संदेश-पासिंग संचार के माध्यम से एक दूसरे के साथ बातचीत करते हैं। हालांकि, सीएसपी नाम का अनुक्रमिक हिस्सा अब  मिथ्या नाम है, क्योंकि आधुनिक सीएसपी घटक प्रक्रियाओं को अनुक्रमिक प्रक्रियाओं के रूप में और अधिक आदिम प्रक्रियाओं की समानांतर संरचना के रूप में परिभाषित करने की अनुमति देता है। विभिन्न प्रक्रियाओं के बीच संबंध, और जिस तरह से प्रत्येक प्रक्रिया अपने पर्यावरण के साथ संचार करती है, उसे विभिन्न [[प्रक्रिया गणना]] ऑपरेटरों का उपयोग करके वर्णित किया गया है। इस बीजगणितीय दृष्टिकोण का उपयोग करते हुए, कुछ आदिम तत्वों से काफी जटिल प्रक्रिया विवरणों का निर्माण आसानी से किया जा सकता है।
 === आदिम ===
@@ Line 79: / Line 79: @@
 === बीजगणितीय ऑपरेटर ===
-सीएसपी में बीजगणितीय ऑपरेटरों की एक विस्तृत श्रृंखला है। प्रमुख हैं:
+सीएसपी में बीजगणितीय ऑपरेटरों की  विस्तृत श्रृंखला है। प्रमुख हैं:
 ; उपसर्ग
-: उपसर्ग ऑपरेटर एक नई प्रक्रिया का उत्पादन करने के लिए एक घटना और एक प्रक्रिया को जोड़ता है। उदाहरण के लिए, <math display="block">a \to P</math> वह प्रक्रिया है जो संवाद करने को तैयार है {{mvar|a}} अपने पर्यावरण के साथ और उसके बाद {{mvar|a}}, प्रक्रिया की तरह व्यवहार करता है {{mvar|P}}.
+: उपसर्ग ऑपरेटर  नई प्रक्रिया का उत्पादन करने के लिए  घटना और  प्रक्रिया को जोड़ता है। उदाहरण के लिए, <math display="block">a \to P</math> वह प्रक्रिया है जो संवाद करने को तैयार है {{mvar|a}} अपने पर्यावरण के साथ और उसके बाद {{mvar|a}}, प्रक्रिया की तरह व्यवहार करता है {{mvar|P}}.
 ; नियतात्मक पसंद
-: नियतात्मक (या बाहरी) पसंद ऑपरेटर एक प्रक्रिया के भविष्य के विकास को दो घटक प्रक्रियाओं के बीच एक विकल्प के रूप में परिभाषित करने की अनुमति देता है और पर्यावरण को किसी एक प्रक्रिया के लिए प्रारंभिक घटना को संप्रेषित करके पसंद को हल करने की अनुमति देता है। उदाहरण के लिए, <math display="block">(a \to P) \Box (b \to Q)</math> वह प्रक्रिया है जो प्रारंभिक घटनाओं को संप्रेषित करने के लिए तैयार है {{mvar|a}} और {{mvar|b}} और बाद में या तो व्यवहार करता है {{mvar|P}} या {{mvar|Q}}, पर्यावरण किस प्रारंभिक घटना के आधार पर संवाद करना चुनता है। अगर दोनों {{mvar|a}} और {{mvar|b}} को एक साथ संप्रेषित किया गया था, तो विकल्प को गैर-निर्धारित रूप से हल किया जाएगा।
+: नियतात्मक (या बाहरी) पसंद ऑपरेटर  प्रक्रिया के भविष्य के विकास को दो घटक प्रक्रियाओं के बीच एक विकल्प के रूप में परिभाषित करने की अनुमति देता है और पर्यावरण को किसी  प्रक्रिया के लिए प्रारंभिक घटना को संप्रेषित करके पसंद को हल करने की अनुमति देता है। उदाहरण के लिए, <math display="block">(a \to P) \Box (b \to Q)</math> वह प्रक्रिया है जो प्रारंभिक घटनाओं को संप्रेषित करने के लिए तैयार है {{mvar|a}} और {{mvar|b}} और बाद में या तो व्यवहार करता है {{mvar|P}} या {{mvar|Q}}, पर्यावरण किस प्रारंभिक घटना के आधार पर संवाद करना चुनता है। अगर दोनों {{mvar|a}} और {{mvar|b}} को एक साथ संप्रेषित किया गया था, तो विकल्प को गैर-निर्धारित रूप से हल किया जाएगा।
 ; गैर नियतात्मक विकल्प
-: nondeterministic (या आंतरिक) पसंद ऑपरेटर एक प्रक्रिया के भविष्य के विकास को दो घटक प्रक्रियाओं के बीच एक विकल्प के रूप में परिभाषित करने की अनुमति देता है, लेकिन पर्यावरण को किसी भी नियंत्रण की अनुमति नहीं देता है कि कौन से घटक प्रक्रियाओं का चयन किया जाएगा। उदाहरण के लिए, <math display="block">(a \to P) \sqcap (b \to Q)</math> जैसा व्यवहार कर सकता है <math>(a \to P)</math> या <math>(b \to Q)</math>. मानने से इंकार कर सकता है {{mvar|a}} या {{mvar|b}} और संवाद करने के लिए तभी बाध्य है जब पर्यावरण दोनों प्रदान करता है {{mvar|a}} और {{mvar|b}}. यदि पसंद के दोनों पक्षों की प्रारंभिक घटनाएँ समान हैं, तो गैर-नियतात्मकता को अनजाने में एक नाममात्र नियतात्मक पसंद में पेश किया जा सकता है। तो, उदाहरण के लिए, <math display="block">(a \to a \to \text{STOP}) \Box (a \to b \to \text{STOP})</math> के बराबर है <math display="block">a \to \big((a \to \text{STOP}) \sqcap (b \to \text{STOP})\big)</math>
+: nondeterministic (या आंतरिक) पसंद ऑपरेटर  प्रक्रिया के भविष्य के विकास को दो घटक प्रक्रियाओं के बीच  विकल्प के रूप में परिभाषित करने की अनुमति देता है, लेकिन पर्यावरण को किसी भी नियंत्रण की अनुमति नहीं देता है कि कौन से घटक प्रक्रियाओं का चयन किया जाएगा। उदाहरण के लिए, <math display="block">(a \to P) \sqcap (b \to Q)</math> जैसा व्यवहार कर सकता है <math>(a \to P)</math> या <math>(b \to Q)</math>. मानने से इंकार कर सकता है {{mvar|a}} या {{mvar|b}} और संवाद करने के लिए तभी बाध्य है जब पर्यावरण दोनों प्रदान करता है {{mvar|a}} और {{mvar|b}}. यदि पसंद के दोनों पक्षों की प्रारंभिक घटनाएँ समान हैं, तो गैर-नियतात्मकता को अनजाने में  नाममात्र नियतात्मक पसंद में पेश किया जा सकता है। तो, उदाहरण के लिए, <math display="block">(a \to a \to \text{STOP}) \Box (a \to b \to \text{STOP})</math> के बराबर है <math display="block">a \to \big((a \to \text{STOP}) \sqcap (b \to \text{STOP})\big)</math>
 ; इंटरलिविंग
 : इंटरलीविंग ऑपरेटर पूरी तरह से स्वतंत्र समवर्ती गतिविधि का प्रतिनिधित्व करता है। प्रक्रिया <math display="block">P \;|||\; Q</math> दोनों के रूप में व्यवहार करता है {{mvar|P}} और {{mvar|Q}} इसके साथ ही। दोनों प्रक्रियाओं की घटनाओं को मनमाने ढंग से समय के साथ जोड़ा जाता है।
@@ Line 92: / Line 92: @@
 : इंटरफ़ेस समानांतर ऑपरेटर समवर्ती गतिविधि का प्रतिनिधित्व करता है जिसके लिए घटक प्रक्रियाओं के बीच सिंक्रनाइज़ेशन की आवश्यकता होती है: इंटरफ़ेस सेट में कोई भी घटना तभी हो सकती है जब सभी घटक प्रक्रियाएँ उस घटना में संलग्न होने में सक्षम हों। उदाहरण के लिए, प्रक्रिया <math display="block">P \;|[\{ a \}]|\; Q</math> इसकी आवश्यकता है {{mvar|P}} और {{mvar|Q}} दोनों को ईवेंट करने में सक्षम होना चाहिए {{mvar|a}} उस घटना के घटित होने से पहले। तो, उदाहरण के लिए, प्रक्रिया <math display="block">(a \to P) \;|[\{ a \}]|\; (a \to Q)</math> आयोजन में शामिल हो सकते हैं {{mvar|a}} और प्रक्रिया बनें <math display="block">P \;|[\{ a \}]|\; Q</math> जबकि <math display="block">(a \to P ) \;|[\{ a, b \}]|\; (b \to Q)</math> बस गतिरोध होगा।
 ; छुपा रहे है
-: छुपाने वाला ऑपरेटर कुछ घटनाओं को अप्राप्य बनाकर अमूर्त प्रक्रियाओं का एक तरीका प्रदान करता है। छिपाने का एक तुच्छ उदाहरण है <math display="block">(a \to P) \setminus \{ a \}</math> जो, यह मानते हुए कि घटना {{mvar|a}} में दिखाई नहीं देता {{mvar|P}}, बस इतना कम कर देता है <math display="block">P</math>
+: छुपाने वाला ऑपरेटर कुछ घटनाओं को अप्राप्य बनाकर अमूर्त प्रक्रियाओं का  तरीका प्रदान करता है। छिपाने का  सामान्य उदाहरण है <math display="block">(a \to P) \setminus \{ a \}</math> जो, यह मानते हुए कि घटना {{mvar|a}} में दिखाई नहीं देता {{mvar|P}}, बस इतना कम कर देता है <math display="block">P</math>
 === उदाहरण ===
-मूलरूप सीएसपी उदाहरणों में से एक चॉकलेट वेंडिंग मशीन का एक सार प्रतिनिधित्व है और कुछ चॉकलेट खरीदने के इच्छुक व्यक्ति के साथ इसकी बातचीत है। यह वेंडिंग मशीन दो अलग-अलग घटनाओं, "कॉइन" और "चोक" को अंजाम देने में सक्षम हो सकती है, जो क्रमशः भुगतान की प्रविष्टि और चॉकलेट की डिलीवरी का प्रतिनिधित्व करती हैं। एक मशीन जो चॉकलेट देने से पहले भुगतान (केवल नकद में) की मांग करती है, उसे इस प्रकार लिखा जा सकता है:
+मूलरूप सीएसपी उदाहरणों में से  चॉकलेट वेंडिंग मशीन का एक सार प्रतिनिधित्व है और कुछ चॉकलेट खरीदने के इच्छुक व्यक्ति के साथ इसकी बातचीत है। यह वेंडिंग मशीन दो अलग-अलग घटनाओं, "कॉइन" और "चोक" को अंजाम देने में सक्षम हो सकती है, जो क्रमशः भुगतान की प्रविष्टि और चॉकलेट की डिलीवरी का प्रतिनिधित्व करती हैं। एक मशीन जो चॉकलेट देने से पहले भुगतान (केवल नकद में) की मांग करती है, उसे इस प्रकार लिखा जा सकता है:
 <math display="block">\mathrm{VendingMachine} = \mathrm{coin} \rightarrow \mathrm{choc} \rightarrow \mathrm{STOP}</math>
-एक व्यक्ति जो भुगतान करने के लिए एक सिक्के या कार्ड का उपयोग करना चुन सकता है, उसे इस प्रकार मॉडल किया जा सकता है:
+एक व्यक्ति जो भुगतान करने के लिए  सिक्के या कार्ड का उपयोग करना चुन सकता है, उसे इस प्रकार मॉडल किया जा सकता है:
 <math display="block">\mathrm{Person} = (\mathrm{coin} \rightarrow \mathrm{STOP}) \Box (\mathrm{card} \rightarrow \mathrm{STOP})</math>
-इन दोनों प्रक्रियाओं को समानांतर में रखा जा सकता है, ताकि वे एक दूसरे के साथ बातचीत कर सकें। समग्र प्रक्रिया का व्यवहार उन घटनाओं पर निर्भर करता है जिन पर दो घटक प्रक्रियाओं को सिंक्रनाइज़ करना चाहिए। इस प्रकार,
+इन दोनों प्रक्रियाओं को समानांतर में रखा जा सकता है, ताकि वे  दूसरे के साथ बातचीत कर सकें। समग्र प्रक्रिया का व्यवहार उन घटनाओं पर निर्भर करता है जिन पर दो घटक प्रक्रियाओं को सिंक्रनाइज़ करना चाहिए। इस प्रकार,
 <math display="block">\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}</math>
@@ Line 114: / Line 114: @@
 <math display="block">\left (\mathrm{choc} \rightarrow \mathrm{STOP}\right ) \sqcap \mathrm{STOP}</math>
-यह एक ऐसी प्रक्रिया है जो या तो "चोक" घटना की पेशकश करती है और फिर रुक जाती है, या बस रुक जाती है। दूसरे शब्दों में, यदि हम अमूर्तता को सिस्टम के बाहरी दृश्य के रूप में मानते हैं (उदाहरण के लिए, कोई व्यक्ति जो व्यक्ति द्वारा किए गए निर्णय को नहीं देखता है), गैर-नियतात्मक एल्गोरिदम पेश किया गया है।
+यह  ऐसी प्रक्रिया है जो या तो "चोक" घटना की पेशकश करती है और फिर रुक जाती है, या बस रुक जाती है। दूसरे शब्दों में, यदि हम अमूर्तता को सिस्टम के बाहरी दृश्य के रूप में मानते हैं (उदाहरण के लिए, कोई व्यक्ति जो व्यक्ति द्वारा किए गए निर्णय को नहीं देखता है), गैर-नियतात्मक एल्गोरिदम पेश किया गया है।
 == औपचारिक परिभाषा ==
 === सिंटेक्स ===
-CSP का सिंटैक्स "कानूनी" तरीकों को परिभाषित करता है जिसमें प्रक्रियाओं और घटनाओं को जोड़ा जा सकता है। होने देना {{mvar|e}} एक घटना हो, और {{mvar|X}} घटनाओं का एक सेट हो। तब CSP के मूल सिंटैक्स को इस प्रकार परिभाषित किया जा सकता है:
+CSP का सिंटैक्स "कानूनी" तरीकों को परिभाषित करता है जिसमें प्रक्रियाओं और घटनाओं को जोड़ा जा सकता है। माना {{mvar|e}} एक घटना हो, और {{mvar|X}}  घटनाओं का  सेट हो। तब CSP के मूल सिंटैक्स को इस प्रकार परिभाषित किया जा सकता है:
 <math display="block">
@@ Line 145: / Line 145: @@
 सीएसपी के तीन प्रमुख डेनोटेशनल मॉडल ट्रेस मॉडल, स्थिर विफलता मॉडल और विफलता/विचलन मॉडल हैं। इन तीन मॉडलों में से प्रत्येक के लिए प्रक्रिया अभिव्यक्तियों से सिमेंटिक मैपिंग सीएसपी के लिए अर्थ संबंधी शब्दार्थ प्रदान करते हैं।<ref name="roscoe" />
-निशान मॉडल एक प्रक्रिया अभिव्यक्ति के अर्थ को घटनाओं (निशान) के अनुक्रमों के सेट के रूप में परिभाषित करता है जिसे प्रदर्शन करने के लिए प्रक्रिया देखी जा सकती है। उदाहरण के लिए,
+निशान मॉडल  प्रक्रिया अभिव्यक्ति के अर्थ को घटनाओं (निशान) के अनुक्रमों के सेट के रूप में परिभाषित करता है जिसे प्रदर्शन करने के लिए प्रक्रिया देखी जा सकती है। उदाहरण के लिए,
 * <math>\mathrm{traces}\left(\mathrm{STOP}\right) = \left\{ \langle\rangle \right\}</math> तब से <math>\mathrm{STOP}</math> कोई आयोजन नहीं करता
 * <math>\mathrm{traces}\left(a\rightarrow b \rightarrow \mathrm{STOP}\right) = \left\{\langle\rangle ,\langle a \rangle, \langle a, b \rangle \right\}</math> प्रक्रिया के बाद से <math>(a\rightarrow b \rightarrow \mathrm{STOP})</math> यह देखा जा सकता है कि कोई घटना नहीं हुई है, घटना {{mvar|a}}, या घटनाओं का क्रम {{mvar|a}} के बाद {{mvar|b}}
-अधिक औपचारिक रूप से, एक प्रक्रिया का अर्थ {{mvar|P}ट्रेसेस मॉडल में } के रूप में परिभाषित किया गया है <math>\mathrm{traces}\left(P\right) \subseteq \Sigma^{\ast}</math> ऐसा है कि:
+<nowiki>अधिक औपचारिक रूप से,  प्रक्रिया का अर्थ {{mvar|P}ट्रेसेस मॉडल में } के रूप में परिभाषित किया गया है </nowiki><math>\mathrm{traces}\left(P\right) \subseteq \Sigma^{\ast}</math> ऐसा है कि:
 # <math>\langle\rangle \in \mathrm{traces}\left(P\right)</math> (अर्थात। <math>\mathrm{traces}\left(P\right)</math> खाली अनुक्रम शामिल है)
 # <math>s_1 \smallfrown s_2 \in \mathrm{traces}\left(P\right) \implies s_1 \in \mathrm{traces}\left(P\right)</math> (अर्थात। <math>\mathrm{traces}\left(P\right)</math> उपसर्ग-बंद है)
 कहाँ <math>\Sigma^{\ast}</math> घटनाओं के सभी संभावित परिमित अनुक्रमों का समुच्चय है।
-स्थिर विफलता मॉडल इनकार करने वाले सेट के साथ निशान मॉडल का विस्तार करता है, जो घटनाओं के सेट हैं <math>X \subseteq \Sigma</math> कि एक प्रक्रिया प्रदर्शन करने से इंकार कर सकती है। असफलता एक जोड़ी है <math>\left(s,X\right)</math>, एक निशान से मिलकर {{mvar|s}}, और एक इनकार सेट {{mvar|X}} जो उन घटनाओं की पहचान करता है जो ट्रेस को निष्पादित करने के बाद एक प्रक्रिया से इनकार कर सकती हैं {{mvar|s}}. स्थिर विफलता मॉडल में एक प्रक्रिया के देखे गए व्यवहार को जोड़ी द्वारा वर्णित किया गया है <math>\left(\mathrm{traces}\left(P\right), \mathrm{failures}\left(P\right)\right)</math>. उदाहरण के लिए,
+स्थिर विफलता मॉडल इनकार करने वाले सेट के साथ निशान मॉडल का विस्तार करता है, जो घटनाओं के सेट हैं <math>X \subseteq \Sigma</math> कि  प्रक्रिया प्रदर्शन करने से इंकार कर सकती है। असफलता एक जोड़ी है <math>\left(s,X\right)</math>, एक निशान से मिलकर {{mvar|s}}, और  इनकार सेट {{mvar|X}} जो उन घटनाओं की पहचान करता है जो ट्रेस को निष्पादित करने के बाद एक प्रक्रिया से इनकार कर सकती हैं {{mvar|s}}. स्थिर विफलता मॉडल में एक प्रक्रिया के देखे गए व्यवहार को जोड़ी द्वारा वर्णित किया गया है <math>\left(\mathrm{traces}\left(P\right), \mathrm{failures}\left(P\right)\right)</math>. उदाहरण के लिए,
 <math display="block">\mathrm{failures}\left(\left(a \rightarrow \mathrm{STOP}\right) \Box \left(b \rightarrow \mathrm{STOP}\right)\right) = \left\{\left(\langle\rangle,\emptyset\right), \left(\langle a \rangle, \left\{a,b\right\}\right), \left(\langle b \rangle,\left\{a,b\right\}\right) \right\}</math>
@@ Line 162: / Line 162: @@
 == उपकरण ==
-वर्षों से, सीएसपी का उपयोग करके वर्णित प्रणालियों के विश्लेषण और समझने के लिए कई उपकरण तैयार किए गए हैं। प्रारंभिक उपकरण कार्यान्वयन ने CSP के लिए विभिन्न प्रकार के मशीन-पठनीय सिंटैक्स का उपयोग किया, जिससे विभिन्न उपकरणों के लिए लिखी गई इनपुट फाइलें असंगत हो गईं। हालाँकि, अधिकांश CSP उपकरण अब ब्रायन स्कैटरगूड द्वारा तैयार की गई CSP की मशीन-पठनीय बोली पर मानकीकृत हो गए हैं, जिसे कभी-कभी CSP के रूप में संदर्भित किया जाता है।<sub>''M''</sub>.<ref>{{Cite journal|author=Scattergood, J.B.|title=मशीन-पठनीय सीएसपी का शब्दार्थ और कार्यान्वयन|version=D.Phil.|publisher=[[Oxford University Computing Laboratory]] | year=1998}}</ref> सीएसपी<sub>''M''</sub> सीएसपी की बोली में औपचारिक रूप से परिभाषित परिचालन शब्दार्थ है, जिसमें एक एम्बेडेड [[कार्यात्मक प्रोग्रामिंग भाषा]] शामिल है।
+वर्षों से, सीएसपी का उपयोग करके वर्णित प्रणालियों के विश्लेषण और समझने के लिए कई उपकरण तैयार किए गए हैं। प्रारंभिक उपकरण कार्यान्वयन ने CSP के लिए विभिन्न प्रकार के मशीन-पठनीय सिंटैक्स का उपयोग किया, जिससे विभिन्न उपकरणों के लिए लिखी गई इनपुट फाइलें असंगत हो गईं। हालाँकि, अधिकांश CSP उपकरण अब ब्रायन स्कैटरगूड द्वारा तैयार की गई CSP की मशीन-पठनीय बोली पर मानकीकृत हो गए हैं, जिसे कभी-कभी CSP के रूप में संदर्भित किया जाता है।<sub>''M''</sub>.<ref>{{Cite journal|author=Scattergood, J.B.|title=मशीन-पठनीय सीएसपी का शब्दार्थ और कार्यान्वयन|version=D.Phil.|publisher=[[Oxford University Computing Laboratory]] | year=1998}}</ref> सीएसपी<sub>''M''</sub> सीएसपी की बोली में औपचारिक रूप से परिभाषित परिचालन शब्दार्थ है, जिसमें  एम्बेडेड [[कार्यात्मक प्रोग्रामिंग भाषा]] शामिल है।
-सबसे प्रसिद्ध सीएसपी उपकरण शायद फेल्योर/डाइवर्जेंस रिफाइनमेंट 2 (एफडीआर2) है, जो फॉर्मल सिस्टम्स (यूरोप) लिमिटेड द्वारा विकसित एक वाणिज्यिक उत्पाद है। एफडीआर2 को अक्सर एक [[मॉडल चेकर]] के रूप में वर्णित किया जाता है, लेकिन तकनीकी रूप से इसमें एक शोधन जांचकर्ता है। यह दो सीएसपी प्रक्रिया अभिव्यक्तियों को लेबल किए गए संक्रमण प्रणाली (एलटीएस) में परिवर्तित करता है, और फिर यह निर्धारित करता है कि प्रक्रियाओं में से एक कुछ निर्दिष्ट सिमेंटिक मॉडल (निशान, विफलताओं, या विफलताओं/विचलन) के भीतर दूसरे का परिशोधन है या नहीं।<ref>{{Cite journal|author=A.W. Roscoe|title=मॉडल-चेकिंग सीएसपी|version=In ''A Classical Mind: essays in Honour of C.A.R. Hoare''|publisher=Prentice Hall|year=1994|author-link=Bill Roscoe}}</ref> FDR2 राज्य-स्थान के आकार को कम करने के लिए एलटीएस प्रक्रिया के लिए विभिन्न राज्य-स्थान संपीड़न एल्गोरिदम लागू करता है जिसे शोधन जांच के दौरान खोजा जाना चाहिए। FDR2 को FDR3 द्वारा सफल किया गया है, एक पूरी तरह से फिर से लिखा गया संस्करण है जिसमें समानांतर निष्पादन और एक एकीकृत प्रकार चेकर शामिल है। यह ऑक्सफोर्ड विश्वविद्यालय द्वारा जारी किया गया है, जिसने 2008-12 की अवधि में FDR2 भी जारी किया था।<ref>{{cite web|url=https://www.cs.ox.ac.uk/projects/fdr/manual/introduction.html|title=Introduction — FDR 4.2.4 documentation|website=www.cs.ox.ac.uk}}</ref>
+सबसे प्रसिद्ध सीएसपी उपकरण शायद फेल्योर/डाइवर्जेंस रिफाइनमेंट 2 (एफडीआर2) है, जो फॉर्मल सिस्टम्स (यूरोप) लिमिटेड द्वारा विकसित  वाणिज्यिक उत्पाद है। एफडीआर2 को अक्सर  [[मॉडल चेकर]] के रूप में वर्णित किया जाता है, लेकिन तकनीकी रूप से इसमें एक शोधन जांचकर्ता है। यह दो सीएसपी प्रक्रिया अभिव्यक्तियों को लेबल किए गए संक्रमण प्रणाली (एलटीएस) में परिवर्तित करता है, और फिर यह निर्धारित करता है कि प्रक्रियाओं में से  कुछ निर्दिष्ट सिमेंटिक मॉडल (निशान, विफलताओं, या विफलताओं/विचलन) के भीतर दूसरे का परिशोधन है या नहीं।<ref>{{Cite journal|author=A.W. Roscoe|title=मॉडल-चेकिंग सीएसपी|version=In ''A Classical Mind: essays in Honour of C.A.R. Hoare''|publisher=Prentice Hall|year=1994|author-link=Bill Roscoe}}</ref> FDR2 राज्य-स्थान के आकार को कम करने के लिए एलटीएस प्रक्रिया के लिए विभिन्न राज्य-स्थान संपीड़न एल्गोरिदम लागू करता है जिसे शोधन जांच के दौरान खोजा जाना चाहिए। FDR2 को FDR3 द्वारा सफल किया गया है,  पूरी तरह से फिर से लिखा गया संस्करण है जिसमें समानांतर निष्पादन और  एकीकृत प्रकार चेकर शामिल है। यह ऑक्सफोर्ड विश्वविद्यालय द्वारा जारी किया गया है, जिसने 2008-12 की अवधि में FDR2 भी जारी किया था।<ref>{{cite web|url=https://www.cs.ox.ac.uk/projects/fdr/manual/introduction.html|title=Introduction — FDR 4.2.4 documentation|website=www.cs.ox.ac.uk}}</ref>
-एडिलेड शोधन परीक्षक (एआरसी)<ref>{{cite conference |first1=Atanas N. |last1=  Parashkevov| first2 = Jay | last2 = Yantchev |title=ARC – a tool for efficient refinement and equivalence checking for CSP |book-title=IEEE Int. Conf. on Algorithms and Architectures for Parallel Processing ICA3PP '96 |pages= 68–75|year=1996 |citeseerx = 10.1.1.45.3212 }}</ref> एडीलेड विश्वविद्यालय में औपचारिक मॉडलिंग और सत्यापन समूह द्वारा विकसित एक सीएसपी शोधन परीक्षक है। ARC, FDR2 से इस मायने में भिन्न है कि यह आंतरिक रूप से CSP प्रक्रियाओं को [[ द्विआधारी निर्णय आरेख ]] (OBDDs) के रूप में प्रस्तुत करता है, जो राज्य-अंतरिक्ष संपीड़न एल्गोरिदम जैसे कि FDR2 में उपयोग किए जाने वाले एल्गोरिदम के उपयोग की आवश्यकता के बिना स्पष्ट LTS अभ्यावेदन की राज्य विस्फोट समस्या को कम करता है।
+एडिलेड शोधन परीक्षक (एआरसी)<ref>{{cite conference |first1=Atanas N. |last1=  Parashkevov| first2 = Jay | last2 = Yantchev |title=ARC – a tool for efficient refinement and equivalence checking for CSP |book-title=IEEE Int. Conf. on Algorithms and Architectures for Parallel Processing ICA3PP '96 |pages= 68–75|year=1996 |citeseerx = 10.1.1.45.3212 }}</ref> एडीलेड विश्वविद्यालय में औपचारिक मॉडलिंग और सत्यापन समूह द्वारा विकसित  सीएसपी शोधन परीक्षक है। ARC, FDR2 से इस मायने में भिन्न है कि यह आंतरिक रूप से CSP प्रक्रियाओं को [[ द्विआधारी निर्णय आरेख ]] (OBDDs) के रूप में प्रस्तुत करता है, जो राज्य-अंतरिक्ष संपीड़न एल्गोरिदम जैसे कि FDR2 में उपयोग किए जाने वाले एल्गोरिदम के उपयोग की आवश्यकता के बिना स्पष्ट LTS अभ्यावेदन की राज्य विस्फोट समस्या को कम करता है।
 प्रोबी परियोजना,<ref>{{cite conference|first1=Michael|last1=Leuschel|first2=Marc|last2=Fontaine|title=Probing the Depths of CSP-M: A new FDR-compliant Validation Tool|book-title=ICFEM 2008|publisher=Springer-Verlag| year=2008| url=http://www.stups.uni-duesseldorf.de/publications/main.pdf|access-date=2008-11-26|url-status=dead|archive-url=https://web.archive.org/web/20110719102153/http://www.stups.uni-duesseldorf.de/publications/main.pdf|archive-date=2011-07-19}}</ref> जिसे Institut für Informatik, Heinrich-Heine-Universität Düsseldorf द्वारा होस्ट किया जाता है, मूल रूप से B विधि में निर्मित विनिर्देशों के विश्लेषण का समर्थन करने के लिए बनाया गया था। हालांकि, इसमें परिशोधन जांच और [[रैखिक लौकिक तर्क]] मॉडल-जांच दोनों के माध्यम से सीएसपी प्रक्रियाओं के विश्लेषण के लिए समर्थन भी शामिल है। ProB का उपयोग संयुक्त CSP और B विनिर्देशों के गुणों को सत्यापित करने के लिए भी किया जा सकता है। एक ProBE CSP एनिमेटर FDR3 में एकीकृत है।
 प्रक्रिया विश्लेषण टूलकिट (पीएटी)
-<ref>{{cite conference | last1 = Sun | first1 = Jun | first2 = Yang | last2 = Liu | first3 = Jin Song | last3 = Dong | title = PAT: Towards Flexible Verification under Fairness | book-title = Proceedings of the 20th International Conference on Computer-Aided Verification (CAV 2009) | publisher = Springer | series = Lecture Notes in Computer Science | volume = 5643 | year = 2009 | url = http://www.comp.nus.edu.sg/~sunj/Publications/cav09.pdf | access-date = 2009-06-16 | url-status = dead | archive-url = https://web.archive.org/web/20110611055744/http://www.comp.nus.edu.sg/~sunj/Publications/cav09.pdf | archive-date = 2011-06-11 }}</ref><ref>{{cite conference | last1 = Sun | first1 = Jun | first2 = Yang | last2 = Liu | first3 = Jin Song | last3 = Dong | title = Model Checking CSP Revisited: Introducing a Process Analysis Toolkit | book-title = Proceedings of the Third International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2008) | pages = 307–322 | publisher = Springer | series = Communications in Computer and Information Science | volume = 17 | year = 2008 | url = http://www.comp.nus.edu.sg/~sunj/Publications/ISoLA08.pdf | access-date = 2009-01-15 | url-status = dead | archive-url = https://web.archive.org/web/20090108091954/http://www.comp.nus.edu.sg/~sunj/Publications/ISoLA08.pdf | archive-date = 2009-01-08 }}</ref> सिंगापुर के राष्ट्रीय विश्वविद्यालय में स्कूल ऑफ कंप्यूटिंग में विकसित एक सीएसपी विश्लेषण उपकरण है। पीएटी परिशोधन जांच, एलटीएल मॉडल-जांच, और सीएसपी और समयबद्ध सीएसपी प्रक्रियाओं का अनुकरण करने में सक्षम है। PAT प्रोसेस लैंग्वेज CSP को म्यूटेबल शेयर्ड वेरिएबल्स, एसिंक्रोनस मैसेज पासिंग, और विभिन्न प्रकार की निष्पक्षता और मात्रात्मक समय से संबंधित प्रक्रिया निर्माणों के समर्थन के साथ विस्तारित करती है जैसे कि <code>deadline</code> और <code>waituntil</code>. पीएटी प्रक्रिया भाषा का अंतर्निहित डिजाइन सिद्धांत प्रक्रियात्मक कार्यक्रमों के साथ एक उच्च स्तरीय विनिर्देश भाषा को जोड़ना है (उदाहरण के लिए पीएटी में एक घटना एक अनुक्रमिक कार्यक्रम या यहां तक कि बाहरी सी # पुस्तकालय कॉल भी हो सकती है) अधिक अभिव्यक्ति के लिए। परिवर्तनीय साझा चर और अतुल्यकालिक चैनल मानक सीएसपी में उपयोग किए जाने वाले प्रसिद्ध प्रक्रिया मॉडलिंग पैटर्न के लिए एक सुविधाजनक [[सिंटैक्टिक चीनी]] प्रदान करते हैं। पीएटी सिंटैक्स समान है, लेकिन सीएसपी के समान नहीं है<sub>''M''</sub>.<ref>{{cite conference |first1=Jun |last1=Sun |first2=Yang |last2=Liu |first3=Jin Song |last3=Dong |first4=Chunqing |last4=Chen |title=सिस्टम विशिष्टता और सत्यापन के लिए विनिर्देशों और कार्यक्रमों को एकीकृत करना|book-title=IEEE Int. Conf. on Theoretical Aspects of Software Engineering TASE '09 |year=2009 |url=http://www.comp.nus.edu.sg/~sunj/Publications/tase09.pdf |access-date=2009-04-13 |url-status=dead |archive-url=https://web.archive.org/web/20110611055219/http://www.comp.nus.edu.sg/~sunj/Publications/tase09.pdf |archive-date=2011-06-11 }}</ref> पीएटी सिंटैक्स और मानक सीएसपी के बीच मुख्य अंतर<sub>''M''</sub> प्रक्रिया अभिव्यक्तियों को समाप्त करने के लिए अर्धविरामों का उपयोग, चर और असाइनमेंट के लिए सिंटैक्टिक चीनी को शामिल करना, और आंतरिक पसंद और समांतर संरचना के लिए थोड़ा अलग वाक्यविन्यास का उपयोग करना है।
+<ref>{{cite conference | last1 = Sun | first1 = Jun | first2 = Yang | last2 = Liu | first3 = Jin Song | last3 = Dong | title = PAT: Towards Flexible Verification under Fairness | book-title = Proceedings of the 20th International Conference on Computer-Aided Verification (CAV 2009) | publisher = Springer | series = Lecture Notes in Computer Science | volume = 5643 | year = 2009 | url = http://www.comp.nus.edu.sg/~sunj/Publications/cav09.pdf | access-date = 2009-06-16 | url-status = dead | archive-url = https://web.archive.org/web/20110611055744/http://www.comp.nus.edu.sg/~sunj/Publications/cav09.pdf | archive-date = 2011-06-11 }}</ref><ref>{{cite conference | last1 = Sun | first1 = Jun | first2 = Yang | last2 = Liu | first3 = Jin Song | last3 = Dong | title = Model Checking CSP Revisited: Introducing a Process Analysis Toolkit | book-title = Proceedings of the Third International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2008) | pages = 307–322 | publisher = Springer | series = Communications in Computer and Information Science | volume = 17 | year = 2008 | url = http://www.comp.nus.edu.sg/~sunj/Publications/ISoLA08.pdf | access-date = 2009-01-15 | url-status = dead | archive-url = https://web.archive.org/web/20090108091954/http://www.comp.nus.edu.sg/~sunj/Publications/ISoLA08.pdf | archive-date = 2009-01-08 }}</ref> सिंगापुर के राष्ट्रीय विश्वविद्यालय में स्कूल ऑफ कंप्यूटिंग में विकसित  सीएसपी विश्लेषण उपकरण है। पीएटी परिशोधन जांच, एलटीएल मॉडल-जांच, और सीएसपी और समयबद्ध सीएसपी प्रक्रियाओं का अनुकरण करने में सक्षम है। PAT प्रोसेस लैंग्वेज CSP को म्यूटेबल शेयर्ड वेरिएबल्स, एसिंक्रोनस मैसेज पासिंग, और विभिन्न प्रकार की निष्पक्षता और मात्रात्मक समय से संबंधित प्रक्रिया निर्माणों के समर्थन के साथ विस्तारित करती है जैसे कि <code>deadline</code> और <code>waituntil</code>. पीएटी प्रक्रिया भाषा का अंतर्निहित डिजाइन सिद्धांत प्रक्रियात्मक कार्यक्रमों के साथ एक उच्च स्तरीय विनिर्देश भाषा को जोड़ना है (उदाहरण के लिए पीएटी में  घटना  अनुक्रमिक कार्यक्रम या यहां तक कि बाहरी सी # पुस्तकालय कॉल भी हो सकती है) अधिक अभिव्यक्ति के लिए। परिवर्तनीय साझा चर और अतुल्यकालिक चैनल मानक सीएसपी में उपयोग किए जाने वाले प्रसिद्ध प्रक्रिया मॉडलिंग पैटर्न के लिए  सुविधाजनक [[सिंटैक्टिक चीनी]] प्रदान करते हैं। पीएटी सिंटैक्स समान है, लेकिन सीएसपी के समान नहीं है<sub>''M''</sub>.<ref>{{cite conference |first1=Jun |last1=Sun |first2=Yang |last2=Liu |first3=Jin Song |last3=Dong |first4=Chunqing |last4=Chen |title=सिस्टम विशिष्टता और सत्यापन के लिए विनिर्देशों और कार्यक्रमों को एकीकृत करना|book-title=IEEE Int. Conf. on Theoretical Aspects of Software Engineering TASE '09 |year=2009 |url=http://www.comp.nus.edu.sg/~sunj/Publications/tase09.pdf |access-date=2009-04-13 |url-status=dead |archive-url=https://web.archive.org/web/20110611055219/http://www.comp.nus.edu.sg/~sunj/Publications/tase09.pdf |archive-date=2011-06-11 }}</ref> पीएटी सिंटैक्स और मानक सीएसपी के बीच मुख्य अंतर<sub>''M''</sub> प्रक्रिया अभिव्यक्तियों को समाप्त करने के लिए अर्धविरामों का उपयोग, चर और असाइनमेंट के लिए सिंटैक्टिक चीनी को शामिल करना, और आंतरिक पसंद और समांतर संरचना के लिए थोड़ा अलग वाक्यविन्यास का उपयोग करना है।
 विजुअलनेट्स<ref>{{cite conference|last1=Green|first1=Mark| first2 = Ali | last2 = Abdallah|title=संचार प्रणालियों के अनुकूलन के लिए प्रदर्शन विश्लेषण और व्यवहार ट्यूनिंग|book-title=Communicating Process Architectures 2002|year=2002|url=https://www.researchgate.net/publication/290383042}}</ref> विनिर्देशों से सीएसपी सिस्टम के एनिमेटेड विज़ुअलाइज़ेशन का उत्पादन करता है, और समयबद्ध सीएसपी का समर्थन करता है।
-Capsim<ref>{{cite conference|last1=Brooke|first1=Phillip| first2 = Richard | last2 = Paige|title=सीएसपीसिम के साथ आलसी अन्वेषण और सीएसपी मॉडल की जांच|book-title=Communicating Process Architectures 2007|year=2007}}</ref> एक आलसी सिम्युलेटर है। यह सीएसपी की जांच मॉडल नहीं करता है, लेकिन बहुत बड़ी (संभावित रूप से अनंत) प्रणालियों की खोज के लिए उपयोगी है।
+Capsim<ref>{{cite conference|last1=Brooke|first1=Phillip| first2 = Richard | last2 = Paige|title=सीएसपीसिम के साथ आलसी अन्वेषण और सीएसपी मॉडल की जांच|book-title=Communicating Process Architectures 2007|year=2007}}</ref>  आलसी सिम्युलेटर है। यह सीएसपी की जांच मॉडल नहीं करता है, लेकिन बहुत बड़ी (संभावित रूप से अनंत) प्रणालियों की खोज के लिए उपयोगी है।
-[http://www.principia-m.com/syncstitch/ SyncStitch] इंटरैक्टिव मॉडलिंग और पर्यावरण विश्लेषण के साथ एक CSP शोधन परीक्षक है। इसमें एक ग्राफिकल स्टेट-ट्रांज़िशन डायग्राम एडिटर है। उपयोगकर्ता प्रक्रियाओं के व्यवहार को न केवल सीएसपी अभिव्यक्तियों बल्कि राज्य-संक्रमण आरेखों के रूप में मॉडल कर सकता है। जाँच के परिणाम को ग्राफ़िक रूप से कम्प्यूटेशन-ट्री के रूप में भी रिपोर्ट किया जाता है और परिधीय निरीक्षण उपकरणों के साथ अंतःक्रियात्मक रूप से विश्लेषण किया जा सकता है। परिशोधन जांच के अलावा, यह डेडलॉक जांच और लाइवलॉक जांच भी कर सकता है।
+[http://www.principia-m.com/syncstitch/ SyncStitch] इंटरैक्टिव मॉडलिंग और पर्यावरण विश्लेषण के साथ एक CSP शोधन परीक्षक है। इसमें  ग्राफिकल स्टेट-ट्रांज़िशन डायग्राम एडिटर है। उपयोगकर्ता प्रक्रियाओं के व्यवहार को न केवल सीएसपी अभिव्यक्तियों बल्कि राज्य-संक्रमण आरेखों के रूप में मॉडल कर सकता है। जाँच के परिणाम को ग्राफ़िक रूप से कम्प्यूटेशन-ट्री के रूप में भी रिपोर्ट किया जाता है और परिधीय निरीक्षण उपकरणों के साथ अंतःक्रियात्मक रूप से विश्लेषण किया जा सकता है। परिशोधन जांच के अलावा, यह डेडलॉक जांच और लाइवलॉक जांच भी कर सकता है।
 == संबंधित औपचारिकताएं ==
@@ Line 185: / Line 185: @@
 * [https://web.archive.org/web/20110514234220/http://www.comp.nus.edu.sg/~dongjs/tcoz.html TCOZ], समयबद्ध सीएसपी और [[ऑब्जेक्ट जेड]] का एकीकरण
 * [https://web.archive.org/web/20110514234221/http://www.cs.york.ac.uk/circus/ Circus], [[प्रोग्रामिंग के एकीकृत सिद्धांत]]ों पर आधारित CSP और Z विनिर्देश भाषा का एकीकरण
-* [http://www.compass-research.eu/approach.html सीएमएल] {{Webarchive|url=https://web.archive.org/web/20200219205126/http://www.compass-research.eu/approach.html |date=2020-02-19 }} (कम्पास मॉडलिंग लैंग्वेज), [https://web.archive.org/web/20110514234221/http://www.cs.york.ac.uk/circus/ Circus] और VDM विनिर्देश भाषा का एक संयोजन विकसित किया गया है। [[सिस्टम की प्रणाली]] (एसओएस) की मॉडलिंग
+* [http://www.compass-research.eu/approach.html सीएमएल] {{Webarchive|url=https://web.archive.org/web/20200219205126/http://www.compass-research.eu/approach.html |date=2020-02-19 }} (कम्पास मॉडलिंग लैंग्वेज), [https://web.archive.org/web/20110514234221/http://www.cs.york.ac.uk/circus/ Circus] और VDM विनिर्देश भाषा का  संयोजन विकसित किया गया है। [[सिस्टम की प्रणाली]] (एसओएस) की मॉडलिंग
-* [https://web.archive.org/web/20110514234221/http://www.cs.swan.ac.uk/~csmarkus/Papers/cspcasl.ps CspCASL], [[सामान्य बीजगणितीय विशिष्टता भाषा]] का एक विस्तार जो एकीकृत करता है सीएसपी
+* [https://web.archive.org/web/20110514234221/http://www.cs.swan.ac.uk/~csmarkus/Papers/cspcasl.ps CspCASL], [[सामान्य बीजगणितीय विशिष्टता भाषा]] का  विस्तार जो एकीकृत करता है सीएसपी
-[[टेम्पोरल ऑर्डरिंग विशिष्टता की भाषा]] भाषा, एक अंतरराष्ट्रीय मानक<ref>[[Language Of Temporal Ordering Specification|ISO 8807, Language of Temporal Ordering Specification]]</ref> जिसमें CSP और कम्युनिकेटिंग सिस्टम्स की कैलकुलस की विशेषताएँ शामिल हैं।
+[[टेम्पोरल ऑर्डरिंग विशिष्टता की भाषा]] भाषा,  अंतरराष्ट्रीय मानक<ref>[[Language Of Temporal Ordering Specification|ISO 8807, Language of Temporal Ordering Specification]]</ref> जिसमें CSP और कम्युनिकेटिंग सिस्टम्स की कैलकुलस की विशेषताएँ शामिल हैं।
-* [https://link.springer.com/chapter/10.1007/978-3-319-05032-4_25 PALPS], [[अन्ना फिलिपो]] द्वारा विकसित पारिस्थितिक मॉडल के लिए स्थानों के साथ एक संभावित विस्तार और {{ill|Mauricio toro bermúdez|es|vertical-align=sup}}
+* [https://link.springer.com/chapter/10.1007/978-3-319-05032-4_25 PALPS], [[अन्ना फिलिपो]] द्वारा विकसित पारिस्थितिक मॉडल के लिए स्थानों के साथ  संभावित विस्तार और {{ill|Mauricio toro bermúdez|es|vertical-align=sup}}
 == [[अभिनेता मॉडल]] के साथ तुलना ==
 जहाँ तक यह संदेशों का आदान-प्रदान करने वाली समवर्ती प्रक्रियाओं से संबंधित है, अभिनेता मॉडल मोटे तौर पर CSP के समान है। हालाँकि, दो मॉडल उनके द्वारा प्रदान किए जाने वाले आदिम के संबंध में कुछ मूलभूत रूप से भिन्न विकल्प बनाते हैं:
 * सीएसपी प्रक्रियाएं गुमनाम होती हैं, जबकि अभिनेताओं की पहचान होती है।
-* सीएसपी संदेश भेजने के लिए स्पष्ट चैनलों का उपयोग करता है, जबकि अभिनेता सिस्टम नामित गंतव्य अभिनेताओं को संदेश प्रेषित करते हैं। इन दृष्टिकोणों को एक दूसरे का दोहरा माना जा सकता है, इस अर्थ में कि एक चैनल के माध्यम से प्राप्त होने वाली प्रक्रियाओं की प्रभावी रूप से उस चैनल के अनुरूप पहचान होती है, जबकि अभिनेताओं के बीच नाम-आधारित युग्मन को चैनलों के रूप में व्यवहार करने वाले अभिनेताओं का निर्माण करके तोड़ा जा सकता है।
+* सीएसपी संदेश भेजने के लिए स्पष्ट चैनलों का उपयोग करता है, जबकि अभिनेता सिस्टम नामित गंतव्य अभिनेताओं को संदेश प्रेषित करते हैं। इन दृष्टिकोणों को एक दूसरे का दोहरा माना जा सकता है, इस अर्थ में कि  चैनल के माध्यम से प्राप्त होने वाली प्रक्रियाओं की प्रभावी रूप से उस चैनल के अनुरूप पहचान होती है, जबकि अभिनेताओं के बीच नाम-आधारित युग्मन को चैनलों के रूप में व्यवहार करने वाले अभिनेताओं का निर्माण करके तोड़ा जा सकता है।
 * सीएसपी संदेश-पासिंग में मूल रूप से संदेश भेजने और प्राप्त करने में शामिल प्रक्रियाओं के बीच एक मेल मिलाप शामिल है, यानी प्रेषक तब तक संदेश प्रेषित नहीं कर सकता जब तक कि रिसीवर इसे स्वीकार करने के लिए तैयार न हो। इसके विपरीत, अभिनेता प्रणालियों में संदेश-पासिंग मौलिक रूप से अतुल्यकालिक है, यानी संदेश संचरण और स्वागत एक ही समय में नहीं होता है, और प्रेषक संदेशों को प्राप्त करने से पहले उन्हें स्वीकार करने के लिए तैयार कर सकते हैं। इन दृष्टिकोणों को एक दूसरे के दोहरे भी माना जा सकता है, इस अर्थ में कि मिलन-स्थल-आधारित प्रणालियों का उपयोग बफ़र संचार के निर्माण के लिए किया जा सकता है जो अतुल्यकालिक संदेश प्रणाली के रूप में व्यवहार करता है, जबकि अतुल्यकालिक प्रणालियों का उपयोग संदेश/ पावती प्रोटोकॉल प्रेषकों और रिसीवरों को सिंक्रनाइज़ करने के लिए।
-ध्यान दें कि उपरोक्त गुण होरे द्वारा मूल सीएसपी पेपर को जरूरी नहीं बताते हैं, बल्कि गोलंग और क्लोजर के core.async जैसे कार्यान्वयन में देखा गया विचार का आधुनिक अवतार है। मूल कागज में, चैनल विनिर्देश का एक केंद्रीय हिस्सा नहीं थे, और प्रेषक और रिसीवर प्रक्रियाएं वास्तव में एक दूसरे को नाम से पहचानती हैं।
+ध्यान दें कि उपरोक्त गुण होरे द्वारा मूल सीएसपी पेपर को जरूरी नहीं बताते हैं, बल्कि गोलंग और क्लोजर के core.async जैसे कार्यान्वयन में देखा गया विचार का आधुनिक अवतार है। मूल कागज में, चैनल विनिर्देश का  केंद्रीय हिस्सा नहीं थे, और प्रेषक और रिसीवर प्रक्रियाएं वास्तव में एक दूसरे को नाम से पहचानती हैं।
 == पुरस्कार ==
-में, "तकनीकी उपलब्धि के लिए [[एलिज़ाबेथ द्वितीय]] का पुरस्कार ... ऑक्सफोर्ड यूनिवर्सिटी कंप्यूटिंग प्रयोगशाला में प्रदान किया गया है। [ऑक्सफोर्ड यूनिवर्सिटी] कंप्यूटिंग प्रयोगशाला। यह पुरस्कार प्रयोगशाला और [[इनमोस]] लिमिटेड के बीच एक सफल सहयोग को मान्यता देता है। ... इनमोस का प्रमुख उत्पाद 'ट्रांसप्यूटर' है, एक [[माइक्रोप्रोसेसर]] जिसमें कई पुर्जे होते हैं जिन्हें सामान्य रूप से एक ही [[इलेक्ट्रॉनिक घटक]] में निर्मित करने की आवश्यकता होती है।<ref>{{cite journal |title= Sharp as a Razor: A Queen's Award for the Computing Laboratory |last1=Geraint Jones |journal=[[The Oxford Magazine]] |issue=59, Fourth Week, Trinity Term |date=1990 |url=http://www.cs.ox.ac.uk/people/geraint.jones/ftp/pub/Documents/techpapers/Geraint.Jones/QATA-1-90.ps|author1-link=Geraint Jones }}</ref> टोनी होरे के अनुसार,<ref>{{cite journal |title= C.A.R के साथ एक साक्षात्कार होरे|url=https://dl.acm.org/doi/abs/10.1145/1467247.1467261 |doi=10.1145/1467247.1467261 |last1=Len Shustek |journal= [[Communications of the ACM]] |volume=52 |issue=3 |date=March 2009 |pages=38–41|s2cid=1868477 }}</ref>
+में, "तकनीकी उपलब्धि के लिए [[एलिज़ाबेथ द्वितीय]] का पुरस्कार ... ऑक्सफोर्ड यूनिवर्सिटी कंप्यूटिंग प्रयोगशाला में प्रदान किया गया है। [ऑक्सफोर्ड यूनिवर्सिटी] कंप्यूटिंग प्रयोगशाला। यह पुरस्कार प्रयोगशाला और [[इनमोस]] लिमिटेड के बीच  सफल सहयोग को मान्यता देता है। ... इनमोस का प्रमुख उत्पाद 'ट्रांसप्यूटर' है,  [[माइक्रोप्रोसेसर]] जिसमें कई पुर्जे होते हैं जिन्हें सामान्य रूप से एक ही [[इलेक्ट्रॉनिक घटक]] में निर्मित करने की आवश्यकता होती है।<ref>{{cite journal |title= Sharp as a Razor: A Queen's Award for the Computing Laboratory |last1=Geraint Jones |journal=[[The Oxford Magazine]] |issue=59, Fourth Week, Trinity Term |date=1990 |url=http://www.cs.ox.ac.uk/people/geraint.jones/ftp/pub/Documents/techpapers/Geraint.Jones/QATA-1-90.ps|author1-link=Geraint Jones }}</ref> टोनी होरे के अनुसार,<ref>{{cite journal |title= C.A.R के साथ एक साक्षात्कार होरे|url=https://dl.acm.org/doi/abs/10.1145/1467247.1467261 |doi=10.1145/1467247.1467261 |last1=Len Shustek |journal= [[Communications of the ACM]] |volume=52 |issue=3 |date=March 2009 |pages=38–41|s2cid=1868477 }}</ref>
 "INMOS ट्रांसप्यूटर विचारों के अवतार के रूप में था ... माइक्रोप्रोसेसरों के निर्माण के लिए जो एक दूसरे के साथ तारों के साथ संवाद कर सकते थे जो उनके टर्मिनलों के बीच फैलेंगे। संस्थापक की दृष्टि थी कि सीएसपी के विचार औद्योगिक शोषण के लिए परिपक्व थे, और उन्होंने प्रोग्रामिंग ट्रांसप्यूटर्स के लिए भाषा का आधार बनाया, जिसे ओकैम (प्रोग्रामिंग भाषा) कहा जाता था। … कंपनी का अनुमान है कि इससे उन्हें एक साल पहले हार्डवेयर देने में मदद मिली, अन्यथा ऐसा नहीं होता। उन्होंने ऑक्सफोर्ड यूनिवर्सिटी कंप्यूटिंग प्रयोगशाला के संयोजन के साथ तकनीकी उपलब्धि के लिए रानी का पुरस्कार जीता और आवेदन किया।
@@ Line 208: / Line 208: @@
 * [[एक्ससी प्रोग्रामिंग भाषा]]
 * [[वेरिलॉगसीएसपी]] [[ मैक्रो (कंप्यूटर विज्ञान) ]] का एक सेट है जो [[वेरिलॉग एचडीएल]] में जोड़ा गया है ताकि अनुक्रमिक प्रक्रियाओं चैनल संचार संचार का समर्थन किया जा सके।
-* [[ जॉयस (प्रोग्रामिंग भाषा) ]] सीएसपी के सिद्धांतों पर आधारित एक प्रोग्रामिंग लैंग्वेज है, जिसे 1989 के आसपास [[ब्रिनच हैनसेन]] द्वारा विकसित किया गया था।
+* [[ जॉयस (प्रोग्रामिंग भाषा) ]] सीएसपी के सिद्धांतों पर आधारित  प्रोग्रामिंग लैंग्वेज है, जिसे 1989 के आसपास [[ब्रिनच हैनसेन]] द्वारा विकसित किया गया था।
-* [[सुपरपास्कल]] एक प्रोग्रामिंग लैंग्वेज है जिसे ब्रिन्च हैनसेन द्वारा विकसित किया गया है, जो सीएसपी और जॉयस (प्रोग्रामिंग लैंग्वेज) के साथ उनके पहले के काम से प्रभावित है।
+* [[सुपरपास्कल]]  प्रोग्रामिंग लैंग्वेज है जिसे ब्रिन्च हैनसेन द्वारा विकसित किया गया है, जो सीएसपी और जॉयस (प्रोग्रामिंग लैंग्वेज) के साथ उनके पहले के काम से प्रभावित है।
 * एडा (प्रोग्रामिंग लैंग्वेज) सीएसपी की सुविधाओं को लागू करता है जैसे कि मिलन स्थल।
 * [[डायरेक्टशो]] [[डायरेक्टएक्स]] के अंदर वीडियो ढांचा है, यह ऑडियो और वीडियो फिल्टर को लागू करने के लिए सीएसपी अवधारणाओं का उपयोग करता है।
-* [[OpenCom[[RTOS]]]] एक औपचारिक रूप से विकसित नेटवर्क-केंद्रित वितरित RTOS है जो CSP के व्यावहारिक सुपरसेट पर आधारित है।
+* [[OpenCom[[RTOS]]]]  औपचारिक रूप से विकसित नेटवर्क-केंद्रित वितरित RTOS है जो CSP के व्यावहारिक सुपरसेट पर आधारित है।
 * इनपुट / आउटपुट ऑटोमेटन
 * [[समानांतर प्रोग्रामिंग मॉडल]]
-* [[TLA+]] समवर्ती प्रणालियों के मॉडलिंग और सत्यापन के लिए एक अन्य औपचारिक भाषा है।
+* [[TLA+]] समवर्ती प्रणालियों के मॉडलिंग और सत्यापन के लिए  अन्य औपचारिक भाषा है।
 == संदर्भ ==

v t e Concurrent computing
General	Concurrency Concurrency control Linearizability
Process calculi	CSP CCS ACP LOTOS π-calculus Ambient calculus API-Calculus PEPA Join-calculus
Classic problems	ABA problem Cigarette smokers problem Deadlock Dining philosophers problem Producer–consumer problem Race condition Readers–writers problem Sleeping barber problem
Category: Concurrent computing

Anonymous

Search

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

Namespaces

More

Page actions

Revision as of 11:35, 22 May 2023

Contents