अनुक्रमिक प्रक्रियाओं का संचार करना: Difference between revisions
From Vigyanwiki
No edit summary |
No edit summary |
||
| Line 1: | Line 1: | ||
{{Short description|Formal model in concurrency theory}} | {{Short description|Formal model in concurrency theory}} | ||
{{distinguish|Constraint satisfaction problem}} | {{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"/> [[क्रिस्टल (प्रोग्रामिंग भाषा)]], और [[क्लोजर]] का कोर एसिंक्रोनस है।<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 में [[टोनी होरे]] के लेख में वर्णित किया गया था | |||
सीएसपी को पहली बार 1978 में [[टोनी होरे]] के लेख में वर्णित किया गया था | <ref name="hoare1978">{{cite journal | |||
|last=Hoare | |last=Hoare | ||
|first=C. A. R. | |first=C. A. R. | ||
| Line 13: | Line 14: | ||
|year=1978 | |year=1978 | ||
|doi=10.1145/359576.359585|s2cid=849342 | |doi=10.1145/359576.359585|s2cid=849342 | ||
}}</ref> | }}</ref> किन्तु तब से अधिक सीमा तक विकसित हो गया है।<ref name="25years">{{cite book | ||
|last1=Abdallah | first1 = Ali E.| last2 = Jones | first2 = Cliff B. | last3 = Sanders | first3 = Jeff W. | |last1=Abdallah | first1 = Ali E.| last2 = Jones | first2 = Cliff B. | last3 = Sanders | first3 = Jeff W. | ||
|title=Communicating Sequential Processes: The First 25 Years | |title=Communicating Sequential Processes: The First 25 Years | ||
| Line 21: | Line 22: | ||
|year=2005 | |year=2005 | ||
|url=https://www.springer.com/computer/theoretical+computer+science/foundations+of+computations/book/978-3-540-25813-1 | |url=https://www.springer.com/computer/theoretical+computer+science/foundations+of+computations/book/978-3-540-25813-1 | ||
|isbn=9783540258131}}</ref> सीएसपी व्यावहारिक रूप से उद्योग में [[औपचारिक विनिर्देश]] के लिए एक उपकरण के रूप में विभिन्न प्रणालियों के समवर्ती | |isbn=9783540258131}}</ref> सीएसपी व्यावहारिक रूप से उद्योग में [[औपचारिक विनिर्देश]] के लिए एक उपकरण के रूप में विभिन्न प्रणालियों के समवर्ती , जैसे टी 9000 [[ट्रांसप्यूटर]], के रूप में प्रयुक्त किया गया है।<ref name="barrett">{{cite journal | ||
|last=Barrett | |last=Barrett | ||
|first=G. | |first=G. | ||
| Line 30: | Line 31: | ||
|pages=69–78 | |pages=69–78 | ||
|year=1995 | |year=1995 | ||
|doi=10.1109/32.345823}}</ref> साथ ही सुरक्षित ईकॉमर्स | |doi=10.1109/32.345823}}</ref> साथ ही सुरक्षित ईकॉमर्स प्रणाली <ref name="hall">{{cite journal | ||
|last1 = Hall | |last1 = Hall | ||
|first1=A | |first1=A | ||
| Line 44: | Line 45: | ||
|doi=10.1109/52.976937 | |doi=10.1109/52.976937 | ||
|citeseerx=10.1.1.16.1811 | |citeseerx=10.1.1.16.1811 | ||
}}</ref> सीएसपी का सिद्धांत अभी भी सक्रिय शोध का विषय है | }}</ref> सीएसपी का सिद्धांत अभी भी सक्रिय शोध का विषय है | जिसमें व्यावहारिक प्रयोज्यता की अपनी सीमा को बढ़ाने के लिए काम सम्मिलित है |(उदाहरण के लिए, उन प्रणालियों के मापदंड को बढ़ाना जिनका विश्लेषण किया जा सकता है)।<ref>{{Cite thesis |last = Creese |first = S. |title=Data Independent Induction: CSP Model Checking of Arbitrary Sized Networks |type=D. Phil. |publisher=[[Oxford University]] |year=2001 |citeseerx = 10.1.1.13.7185 }}</ref> | ||
== इतिहास == | == इतिहास == | ||
होरे के मूल 1978 के लेख में प्रस्तुत सीएसपी का संस्करण अनिवार्य रूप से प्रक्रिया कलन के | होरे के मूल 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> मूल सीएसपी में प्रोग्राम निश्चित संख्या में अनुक्रमिक प्रक्रियाओं की समानांतर रचना के रूप में लिखे गए थे | जो एक दूसरे के साथ सख्ती से सिंक्रोनस मैसेज-पासिंग के माध्यम से संचार करते थे। सीएसपी के बाद के संस्करणों के विपरीत, प्रत्येक प्रक्रिया को स्पष्ट नाम दिया गया था, और संदेश के स्रोत या गंतव्य को भेजने या प्राप्त करने की प्रक्रिया के नाम को निर्दिष्ट करके परिभाषित किया गया था। उदाहरण के लिए, प्रक्रिया<syntaxhighlight lang="abl"> | ||
COPY = *[c:character; west?c → east!c] | |||
</syntaxhighlight>नामित प्रक्रिया से बार-बार <code>west</code> अक्षर प्राप्त करता है और उस अक्षर को <code>east</code> नाम की प्रक्रिया के समानांतर रचना में भेजता है |<syntaxhighlight> | |||
[west::DISASSEMBLE || X::COPY || east::ASSEMBLE] | |||
नामित प्रक्रिया से बार-बार | </syntaxhighlight><code>DISASSEMBLE</code> प्रक्रिया के <code>west</code> में नाम निर्दिष्ट करता है | <code>X</code> <code>COPY</code> प्रक्रिया को और <code>east</code> में <code>ASSEMBLE</code> प्रक्रिया को और इन तीन प्रक्रियाओं को समवर्ती रूप से निष्पादित करता है |<ref name="hoare1978" /> | ||
सीएसपी के मूल संस्करण के प्रकाशन के बाद होरे, स्टीफन ब्रूक्स और बिल रोसको|ए. | सीएसपी के मूल संस्करण के प्रकाशन के बाद होरे, स्टीफन ब्रूक्स और बिल रोसको|ए. डब्ल्यू रोस्को ने सीएसपी के सिद्धांत को अपने आधुनिक, प्रक्रिया बीजगणितीय रूप में विकसित और परिष्कृत किया। सीएसपी को प्रक्रिया बीजगणित में विकसित करने के लिए लिया गया दृष्टिकोण [[रॉबिन मिलनर]] के कम्युनिकेटिंग सिस्टम्स (सीसीएस) के कलन पर काम से प्रभावित था और इसके विपरीत सीएसपी का सैद्धांतिक संस्करण प्रारंभ में ब्रुक्स, होरे और रोसको द्वारा 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|साइटसीर]] के अनुसार अब तक का कंप्यूटर विज्ञान संदर्भ था (यद्यपि इसके नमूने की प्रकृति के कारण अविश्वसनीय स्रोत)। होरे की किताब के प्रकाशन के बाद से सीएसपी के सिद्धांत में कुछ छोटे बदलाव हुए हैं। इनमें से अधिकांश परिवर्तन सीएसपी प्रक्रिया विश्लेषण और सत्यापन के लिए स्वचालित उपकरणों के आगमन से प्रेरित थे। रोसको का सिद्धांत और समवर्ती का अभ्यास <ref name="roscoe" /> सीएसपी के इस नए संस्करण का वर्णन करता है। | ||
=== अनुप्रयोग === | === अनुप्रयोग === | ||
सीएसपी का प्रारंभिक और महत्वपूर्ण अनुप्रयोग आईएनएमओएस टी9000 ट्रांसप्यूटर के तत्वों के विनिर्देशन और सत्यापन के लिए इसका उपयोग था | सीएसपी का प्रारंभिक और महत्वपूर्ण अनुप्रयोग आईएनएमओएस टी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" /> | ||
चूंकि सीएसपी जटिल संदेश एक्सचेंजों को | चूंकि सीएसपी जटिल संदेश एक्सचेंजों को सम्मिलित करने वाली प्रणालियों के मॉडलिंग और विश्लेषण के लिए उपयुक्त है | इसलिए इसे संचार और सुरक्षा प्रोटोकॉल के सत्यापन के लिए भी प्रयुक्त किया गया है। इस प्रकार के अनुप्रयोग का प्रमुख उदाहरण लोवे द्वारा सीएसपी और एफडीआर2 शोधन-परीक्षक का उपयोग नीडम-श्रोएडर प्रोटोकॉल प्रमाणीकरण प्रोटोकॉल पर पहले अज्ञात हमले की खोज करने के लिए और फिर सही प्रोटोकॉल विकसित करने के लिए किया जाता है। आक्रमण को परास्त करने में सक्षम है।<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> | ||
== अनौपचारिक विवरण == | == अनौपचारिक विवरण == | ||
जैसा कि इसके नाम से पता चलता है | जैसा कि इसके नाम से पता चलता है | सीएसपी उन घटक प्रक्रियाओं के संदर्भ में प्रणाली के विवरण की अनुमति देता है | जो स्वतंत्र रूप से संचालित होते हैं, और केवल संदेश-पासिंग संचार के माध्यम से एक दूसरे के साथ परस्पर क्रिया करते हैं। चूँकि, सीएसपी नाम का अनुक्रमिक भाग अब मिथ्या नाम है | क्योंकि आधुनिक सीएसपी घटक प्रक्रियाओं को अनुक्रमिक प्रक्रियाओं के रूप में और अधिक प्राचीन प्रक्रियाओं की समानांतर संरचना के रूप में परिभाषित करने की अनुमति देता है। विभिन्न प्रक्रियाओं के बीच संबंध, और जिस तरह से प्रत्येक प्रक्रिया अपने पर्यावरण के साथ संचार करती है | उसे विभिन्न [[प्रक्रिया गणना]] संचालको का उपयोग करके वर्णित किया गया है। इस बीजगणितीय दृष्टिकोण का उपयोग करते हुए, कुछ प्राचीन तत्वों से अधिक जटिल प्रक्रिया विवरणों का निर्माण सरलता से किया जा सकता है। | ||
=== | === प्राचीन === | ||
सीएसपी अपनी प्रक्रिया बीजगणित में प्राचीन के दो वर्ग प्रदान करता है | | |||
; | ;कार्य | ||
:घटनाएँ संचार या | :घटनाएँ संचार या परस्पर क्रिया का प्रतिनिधित्व करती हैं। उन्हें अविभाज्य और तात्कालिक माना जाता है। वे परमाणु नाम (जैसे चालू, बंद), यौगिक नाम (जैसे वाल्व.ओपन, वाल्व.क्लोज़), या इनपुट/आउटपुट इवेंट (जैसे माउस एक्सवाई, स्क्रीन!बिटमैप) हो सकते हैं। | ||
प्राचीन प्रक्रियाएं | |||
: | : प्राचीन प्रक्रियाएं मौलिक व्यवहारों का प्रतिनिधित्व करती हैं | उदाहरणों में विराम (वह प्रक्रिया जो कुछ भी संचार नहीं करती है, जिसे [[गतिरोध]] भी कहा जाता है), और छोडना (जो सफल समाप्ति का प्रतिनिधित्व करता है) सम्मिलित हैं। | ||
=== बीजगणितीय | === बीजगणितीय संचालक === | ||
सीएसपी में बीजगणितीय | सीएसपी में बीजगणितीय संचालको की विस्तृत श्रृंखला है। प्रमुख हैं: | ||
; उपसर्ग | ; उपसर्ग | ||
: उपसर्ग | : उपसर्ग संचालक नई प्रक्रिया का उत्पादन करने के लिए घटना और प्रक्रिया को जोड़ता है। उदाहरण के लिए, <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) \sqcap (b \to Q)</math> जैसा व्यवहार कर सकता है <math>(a \to P)</math> या <math>(b \to Q)</math>. मानने से इंकार कर सकता है {{mvar|a}} या {{mvar|b}} और संचार करने के लिए तभी बाध्य है जब पर्यावरण दोनों प्रदान करता है {{mvar|a}} और {{mvar|b}}. यदि विकल्प के दोनों पक्षों की प्रारंभिक घटनाएँ समान हैं, तो गैर-नियतात्मकता को अनजाने में नाममात्र निर्धारक विकल्प में प्रस्तुत किया जा सकता है। तो, उदाहरण के लिए, | ||
:या तो <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}} इसके साथ ही। दोनों प्रक्रियाओं की घटनाओं को इच्छानुसार समय के साथ जोड़ा जाता है। | ||
; इंटरफ़ेस समानांतर | ; इंटरफ़ेस समानांतर | ||
: इंटरफ़ेस समानांतर | : इंटरफ़ेस समानांतर संचालक समवर्ती गतिविधि का प्रतिनिधित्व करता है जिसके लिए घटक प्रक्रियाओं के बीच सिंक्रनाइज़ेशन की आवश्यकता होती है: इंटरफ़ेस समुच्चय में कोई भी घटना तभी हो सकती है जब सभी घटक प्रक्रियाएँ उस घटना में संलग्न होने में सक्षम हों। उदाहरण के लिए, प्रक्रिया <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|P}} में प्रकट नहीं होने वाली घटना {{mvar|a}} को कम कर देता है |<math display="block">P</math> | ||
=== उदाहरण === | === उदाहरण === | ||
मूलरूप सीएसपी उदाहरणों में से चॉकलेट वेंडिंग मशीन का एक सार प्रतिनिधित्व है और कुछ चॉकलेट खरीदने के इच्छुक व्यक्ति के साथ इसकी | मूलरूप सीएसपी उदाहरणों में से चॉकलेट वेंडिंग मशीन का एक सार प्रतिनिधित्व है और कुछ चॉकलेट खरीदने के इच्छुक व्यक्ति के साथ इसकी परस्पर क्रिया है। यह वेंडिंग मशीन दो अलग-अलग घटनाओं, "कॉइन" और "चोक" को अंजाम देने में सक्षम हो सकती है | जो क्रमशः भुगतान की प्रविष्टि और चॉकलेट की डिलीवरी का प्रतिनिधित्व करती हैं। एक मशीन जो चॉकलेट देने से पहले भुगतान (केवल नकद में) की मांग करती है, उसे इस प्रकार लिखा जा सकता है | | ||
<math display="block">\mathrm{VendingMachine} = \mathrm{coin} \rightarrow \mathrm{choc} \rightarrow \mathrm{STOP}</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{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> | <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 108: | Line 106: | ||
<math display="block">\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 )</math> | <math display="block">\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 )</math> | ||
यदि हम "सिक्का" और "कार्ड" घटनाओं को छिपाकर इस बाद की समग्र प्रक्रिया को | यदि हम "सिक्का" और "कार्ड" घटनाओं को छिपाकर इस बाद की समग्र प्रक्रिया को सार करते हैं, अर्थात | ||
<math display="block">\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\}</math> | <math display="block">\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\}</math> | ||
हमें गैर-नियतात्मक प्रक्रिया मिलती है | हमें गैर-नियतात्मक प्रक्रिया मिलती है | | ||
<math display="block">\left (\mathrm{choc} \rightarrow \mathrm{STOP}\right ) \sqcap \mathrm{STOP}</math> | <math display="block">\left (\mathrm{choc} \rightarrow \mathrm{STOP}\right ) \sqcap \mathrm{STOP}</math> | ||
यह ऐसी प्रक्रिया है जो या तो "चोक" घटना की | यह ऐसी प्रक्रिया है जो या तो "चोक" घटना की प्रस्तुति करती है और फिर रुक जाती है, या बस रुक जाती है। दूसरे शब्दों में, यदि हम अमूर्तता को प्रणाली के बाहरी दृश्य के रूप में मानते हैं (उदाहरण के लिए, कोई व्यक्ति जो व्यक्ति द्वारा किए गए निर्णय को नहीं देखता है), गैर-नियतात्मक एल्गोरिदम प्रस्तुत किया गया है। | ||
== औपचारिक परिभाषा == | == औपचारिक परिभाषा == | ||
=== | === वाक्य - विन्यास === | ||
सीएसपी का वाक्य - विन्यास "नियमबद्ध" विधियों को परिभाषित करता है | जिसमें प्रक्रियाओं और घटनाओं को जोड़ा जा सकता है। माना {{mvar|e}} एक घटना हो, और {{mvar|X}} घटनाओं का समुच्चय हो। तब सीएसपी के मूल वाक्य - विन्यास को इस प्रकार परिभाषित किया जा सकता है | | |||
<math display="block"> | <math display="block"> | ||
| Line 137: | Line 135: | ||
\end{array} | \end{array} | ||
</math> | </math> | ||
ध्यान दें कि, संक्षिप्तता के हित में, ऊपर प्रस्तुत | ध्यान दें कि, संक्षिप्तता के हित में, ऊपर प्रस्तुत वाक्य - विन्यास <math>\mathbf{div}</math> प्रक्रिया को छोड़ देता है, जो [[विचलन (कंप्यूटर विज्ञान)]] के साथ-साथ विभिन्न ऑपरेटरों जैसे वर्णानुक्रमिक समानांतर पाइपिंग और अनुक्रमित विकल्पों का प्रतिनिधित्व करता है। | ||
=== औपचारिक शब्दार्थ === | === औपचारिक शब्दार्थ === | ||
सीएसपी को कई अलग-अलग अर्थ विज्ञान | सीएसपी को कई अलग-अलग अर्थ विज्ञान कंप्यूटर विज्ञान से ओत-प्रोत किया गया है | जो वाक्यगत रूप से सही सीएसपी अभिव्यक्तियों के अर्थ को परिभाषित करता है। सीएसपी के सिद्धांत में पारस्परिक रूप से सुसंगत शब्दार्थ शब्दार्थ, [[बीजगणितीय शब्दार्थ (कंप्यूटर विज्ञान)]], और [[परिचालन शब्दार्थ]] सम्मिलित हैं। | ||
==== सांकेतिक शब्दार्थ ==== | ==== सांकेतिक शब्दार्थ ==== | ||
सीएसपी के तीन प्रमुख | सीएसपी के तीन प्रमुख सांकेतिक मॉडल ट्रेस मॉडल, स्थिर विफलता मॉडल और विफलता/विचलन मॉडल हैं। इन तीन मॉडलों में से प्रत्येक के लिए प्रक्रिया अभिव्यक्तियों से अर्थ मैपिंग सीएसपी के लिए अर्थ संबंधी शब्दार्थ प्रदान करते हैं।<ref name="roscoe" /> | ||
निशान मॉडल प्रक्रिया अभिव्यक्ति के अर्थ को घटनाओं (निशान) के अनुक्रमों के | निशान मॉडल प्रक्रिया अभिव्यक्ति के अर्थ को घटनाओं (निशान) के अनुक्रमों के समुच्चय के रूप में परिभाषित करता है | जिसे प्रदर्शन करने के लिए प्रक्रिया देखी जा सकती है। उदाहरण के लिए, | ||
* <math>\mathrm{traces}\left(\mathrm{STOP}\right) = \left\{ \langle\rangle \right\}</math> तब से <math>\mathrm{STOP}</math> कोई | * <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}} | * <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}} का प्रदर्शन नहीं किया है | ||
अधिक औपचारिक रूप से, ट्रेसेस मॉडल में प्रक्रिया का अर्थ <math>\mathrm{traces}\left(P\right) \subseteq \Sigma^{\ast}</math> P के रूप में परिभाषित किया गया है | ऐसा है कि: | |||
# <math>\langle\rangle \in \mathrm{traces}\left(P\right)</math> (अर्थात। <math>\mathrm{traces}\left(P\right)</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>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 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> | <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><math display="block">\mathrm{failures}\left(\left(a \rightarrow \mathrm{STOP}\right) \sqcap \left(b \rightarrow \mathrm{STOP}\right)\right) = \left\{ \left(\langle\rangle,\left\{a\right\}\right), \left(\langle\rangle,\left\{b\right\}\right), \left(\langle a \rangle, \left\{a,b\right\}\right), \left(\langle b \rangle,\left\{a,b\right\}\right) \right\}</math> | ||
<math display="block">\mathrm{failures}\left(\left(a \rightarrow \mathrm{STOP}\right) \sqcap \left(b \rightarrow \mathrm{STOP}\right)\right) = \left\{ \left(\langle\rangle,\left\{a\right\}\right), \left(\langle\rangle,\left\{b\right\}\right), \left(\langle a \rangle, \left\{a,b\right\}\right), \left(\langle b \rangle,\left\{a,b\right\}\right) \right\}</math> | विफलताओं / विचलन मॉडल आगे विचलन (कंप्यूटर विज्ञान) को संभालने के लिए विफलताओं के मॉडल का विस्तार करता है। विफलताओं/विचलन मॉडल में एक प्रक्रिया का शब्दार्थ एक जोड़ी है <math>\left(\mathrm{failures}_\perp\left(P\right), \mathrm{divergences}\left(P\right)\right)</math> जहाँ <math>\mathrm{divergences}\left(P\right)</math> सभी निशानों के समुच्चय के रूप में परिभाषित किया गया है जो अलग-अलग व्यवहार और <math>\mathrm{failures}_\perp\left(P\right) = \mathrm{failures}\left(P\right) \cup \left\{\left(s,X\right) \mid s \in \mathrm{divergences}\left(P\right)\right\}</math> जन्म दे सकता है | | ||
विफलताओं / विचलन मॉडल आगे विचलन (कंप्यूटर विज्ञान) को संभालने के लिए विफलताओं के मॉडल का विस्तार करता है। विफलताओं/विचलन मॉडल में एक प्रक्रिया का शब्दार्थ एक जोड़ी है <math>\left(\mathrm{failures}_\perp\left(P\right), \mathrm{divergences}\left(P\right)\right)</math> | |||
== उपकरण == | == उपकरण == | ||
वर्षों से, सीएसपी का उपयोग करके वर्णित प्रणालियों के विश्लेषण और समझने के लिए कई उपकरण तैयार किए गए हैं। प्रारंभिक उपकरण कार्यान्वयन ने | वर्षों से, सीएसपी का उपयोग करके वर्णित प्रणालियों के विश्लेषण और समझने के लिए कई उपकरण तैयार किए गए हैं। प्रारंभिक उपकरण कार्यान्वयन ने सीएसपी के लिए विभिन्न प्रकार के मशीन-पठनीय वाक्य - विन्यास का उपयोग किया, जिससे विभिन्न उपकरणों के लिए लिखी गई इनपुट फाइलें असंगत हो गईं। हालाँकि, अधिकांश सीएसपी उपकरण अब ब्रायन स्कैटरगूड द्वारा तैयार की गई सीएसपी की मशीन-पठनीय बोली पर मानकीकृत हो गए हैं, जिसे कभी-कभी सीएसपी के रूप में संदर्भित किया जाता है।<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 को अक्सर [[मॉडल चेकर]] के रूप में वर्णित किया जाता है, | सबसे प्रसिद्ध सीएसपी उपकरण शायद फेल्योर/डाइवर्जेंस रिफाइनमेंट 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 से इस मायने में भिन्न है कि यह आंतरिक रूप से | एडिलेड शोधन परीक्षक (एआरसी)<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 से इस मायने में भिन्न है कि यह आंतरिक रूप से सीएसपी प्रक्रियाओं को [[ द्विआधारी निर्णय आरेख ]] (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 विधि में निर्मित विनिर्देशों के विश्लेषण का समर्थन करने के लिए बनाया गया था। | प्रोबी परियोजना,<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 का उपयोग संयुक्त सीएसपी और B विनिर्देशों के गुणों को सत्यापित करने के लिए भी किया जा सकता है। एक ProBE सीएसपी एनिमेटर 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 प्रोसेस लैंग्वेज | <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 प्रोसेस लैंग्वेज सीएसपी को म्यूटेबल शेयर्ड वेरिएबल्स, एसिंक्रोनस मैसेज पासिंग, और विभिन्न प्रकार की निष्पक्षता और मात्रात्मक समय से संबंधित प्रक्रिया निर्माणों के समर्थन के साथ विस्तारित करती है जैसे कि <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> विनिर्देशों से सीएसपी | विजुअलनेट्स<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] इंटरैक्टिव मॉडलिंग और पर्यावरण विश्लेषण के साथ एक | [http://www.principia-m.com/syncstitch/ SyncStitch] इंटरैक्टिव मॉडलिंग और पर्यावरण विश्लेषण के साथ एक सीएसपी शोधन परीक्षक है। इसमें ग्राफिकल स्टेट-ट्रांज़िशन डायग्राम एडिटर है। उपयोगकर्ता प्रक्रियाओं के व्यवहार को न केवल सीएसपी अभिव्यक्तियों बल्कि राज्य-संक्रमण आरेखों के रूप में मॉडल कर सकता है। जाँच के परिणाम को ग्राफ़िक रूप से कम्प्यूटेशन-ट्री के रूप में भी रिपोर्ट किया जाता है और परिधीय निरीक्षण उपकरणों के साथ अंतःक्रियात्मक रूप से विश्लेषण किया जा सकता है। परिशोधन जांच के अलावा, यह डेडलॉक जांच और लाइवलॉक जांच भी कर सकता है। | ||
== संबंधित औपचारिकताएं == | == संबंधित औपचारिकताएं == | ||
कई अन्य विनिर्देशन भाषाएं और औपचारिकताएं क्लासिक असमय सीएसपी से, या उससे प्रेरित होकर प्राप्त की गई हैं, जिनमें | कई अन्य विनिर्देशन भाषाएं और औपचारिकताएं क्लासिक असमय सीएसपी से, या उससे प्रेरित होकर प्राप्त की गई हैं, जिनमें सम्मिलित हैं: | ||
* [http://citeseer.comp.nus.edu.sg/61363.html समयबद्ध सीएसपी], जिसमें रीयल-टाइम | * [http://citeseer.comp.nus.edu.sg/61363.html समयबद्ध सीएसपी], जिसमें रीयल-टाइम प्रणाली के बारे में तर्क करने के लिए समय संबंधी जानकारी सम्मिलित है | ||
* [https://dx.doi.org/10.1007/BF01178564 रिसेप्टिव प्रोसेस थ्योरी], सीएसपी की विशेषज्ञता जो एसिंक्रोनस (यानी [[ गैर-अवरुद्ध एल्गोरिदम ]]) सेंड ऑपरेशन मानती है | * [https://dx.doi.org/10.1007/BF01178564 रिसेप्टिव प्रोसेस थ्योरी], सीएसपी की विशेषज्ञता जो एसिंक्रोनस (यानी [[ गैर-अवरुद्ध एल्गोरिदम ]]) सेंड ऑपरेशन मानती है | ||
* [https://web.archive.org/web/20110514085953/http://www.wotug.org/paperdb/show_pap.php?f=1&num=394 CSPP] | * [https://web.archive.org/web/20110514085953/http://www.wotug.org/paperdb/show_pap.php?f=1&num=394 CSPP] | ||
* [https://web.archive.org/web/20110514085958/http://www.wotug.org/paperdb/show_pap.php?f=1&num=395 एचसीएसपी] | * [https://web.archive.org/web/20110514085958/http://www.wotug.org/paperdb/show_pap.php?f=1&num=395 एचसीएसपी] | ||
* [https://web.archive.org/web/20110514234220/http://www.comp.nus.edu.sg/~dongjs/tcoz.html TCOZ], समयबद्ध सीएसपी और [[ऑब्जेक्ट जेड]] का एकीकरण | * [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], [[प्रोग्रामिंग के एकीकृत सिद्धांत]]ों पर आधारित | * [https://web.archive.org/web/20110514234221/http://www.cs.york.ac.uk/circus/ Circus], [[प्रोग्रामिंग के एकीकृत सिद्धांत]]ों पर आधारित सीएसपी और 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> जिसमें | [[टेम्पोरल ऑर्डरिंग विशिष्टता की भाषा]] भाषा, अंतरराष्ट्रीय मानक<ref>[[Language Of Temporal Ordering Specification|ISO 8807, Language of Temporal Ordering Specification]]</ref> जिसमें सीएसपी और कम्युनिकेटिंग सिस्टम्स की कैलकुलस की विशेषताएँ सम्मिलित हैं। | ||
* [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}} | ||
== [[अभिनेता मॉडल]] के साथ तुलना == | == [[अभिनेता मॉडल]] के साथ तुलना == | ||
जहाँ तक यह संदेशों का आदान-प्रदान करने वाली समवर्ती प्रक्रियाओं से संबंधित है, अभिनेता मॉडल मोटे तौर पर | जहाँ तक यह संदेशों का आदान-प्रदान करने वाली समवर्ती प्रक्रियाओं से संबंधित है, अभिनेता मॉडल मोटे तौर पर सीएसपी के समान है। हालाँकि, दो मॉडल उनके द्वारा प्रदान किए जाने वाले प्राचीन के संबंध में कुछ मूलभूत रूप से भिन्न विकल्प बनाते हैं: | ||
* सीएसपी प्रक्रियाएं गुमनाम होती हैं, जबकि अभिनेताओं की पहचान होती है। | * सीएसपी प्रक्रियाएं गुमनाम होती हैं, जबकि अभिनेताओं की पहचान होती है। | ||
* सीएसपी संदेश भेजने के लिए स्पष्ट चैनलों का उपयोग करता है, जबकि अभिनेता | * सीएसपी संदेश भेजने के लिए स्पष्ट चैनलों का उपयोग करता है, जबकि अभिनेता प्रणाली नामित गंतव्य अभिनेताओं को संदेश प्रेषित करते हैं। इन दृष्टिकोणों को एक दूसरे का दोहरा माना जा सकता है, इस अर्थ में कि चैनल के माध्यम से प्राप्त होने वाली प्रक्रियाओं की प्रभावी रूप से उस चैनल के अनुरूप पहचान होती है, जबकि अभिनेताओं के बीच नाम-आधारित युग्मन को चैनलों के रूप में व्यवहार करने वाले अभिनेताओं का निर्माण करके तोड़ा जा सकता है। | ||
* सीएसपी संदेश-पासिंग में मूल रूप से संदेश भेजने और प्राप्त करने में | * सीएसपी संदेश-पासिंग में मूल रूप से संदेश भेजने और प्राप्त करने में सम्मिलित प्रक्रियाओं के बीच एक मेल मिलाप सम्मिलित है, यानी प्रेषक तब तक संदेश प्रेषित नहीं कर सकता जब तक कि रिसीवर इसे स्वीकार करने के लिए तैयार न हो। इसके विपरीत, अभिनेता प्रणालियों में संदेश-पासिंग मौलिक रूप से अतुल्यकालिक है, यानी संदेश संचरण और स्वागत एक ही समय में नहीं होता है, और प्रेषक संदेशों को प्राप्त करने से पहले उन्हें स्वीकार करने के लिए तैयार कर सकते हैं। इन दृष्टिकोणों को एक दूसरे के दोहरे भी माना जा सकता है, इस अर्थ में कि मिलन-स्थल-आधारित प्रणालियों का उपयोग बफ़र संचार के निर्माण के लिए किया जा सकता है जो अतुल्यकालिक संदेश प्रणाली के रूप में व्यवहार करता है, जबकि अतुल्यकालिक प्रणालियों का उपयोग संदेश/ पावती प्रोटोकॉल प्रेषकों और रिसीवरों को सिंक्रनाइज़ करने के लिए। | ||
ध्यान दें कि उपरोक्त गुण होरे द्वारा मूल सीएसपी पेपर को जरूरी नहीं बताते हैं, बल्कि गोलंग और क्लोजर के | ध्यान दें कि उपरोक्त गुण होरे द्वारा मूल सीएसपी पेपर को जरूरी नहीं बताते हैं, बल्कि गोलंग और क्लोजर के कोर एसिंक्रोनस जैसे कार्यान्वयन में देखा गया विचार का आधुनिक अवतार है। मूल कागज में, चैनल विनिर्देश का केंद्रीय भाग नहीं थे, और प्रेषक और रिसीवर प्रक्रियाएं वास्तव में एक दूसरे को नाम से पहचानती हैं। | ||
== पुरस्कार == | == पुरस्कार == | ||
1990 में, "तकनीकी उपलब्धि के लिए [[एलिज़ाबेथ द्वितीय]] का पुरस्कार ... ऑक्सफोर्ड यूनिवर्सिटी कंप्यूटिंग प्रयोगशाला में प्रदान किया गया है। [ऑक्सफोर्ड यूनिवर्सिटी] कंप्यूटिंग प्रयोगशाला। यह पुरस्कार प्रयोगशाला और [[इनमोस]] लिमिटेड के बीच सफल सहयोग को मान्यता देता है। ... इनमोस का प्रमुख उत्पाद 'ट्रांसप्यूटर' है, [[माइक्रोप्रोसेसर]] जिसमें कई पुर्जे होते हैं जिन्हें सामान्य रूप से एक ही [[इलेक्ट्रॉनिक घटक]] में निर्मित करने की आवश्यकता होती है।<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> | 1990 में, "तकनीकी उपलब्धि के लिए [[एलिज़ाबेथ द्वितीय]] का पुरस्कार ... ऑक्सफोर्ड यूनिवर्सिटी कंप्यूटिंग प्रयोगशाला में प्रदान किया गया है। [ऑक्सफोर्ड यूनिवर्सिटी] कंप्यूटिंग प्रयोगशाला। यह पुरस्कार प्रयोगशाला और [[इनमोस]] लिमिटेड के बीच सफल सहयोग को मान्यता देता है। ... इनमोस का प्रमुख उत्पाद 'ट्रांसप्यूटर' है, [[माइक्रोप्रोसेसर]] जिसमें कई पुर्जे होते हैं जिन्हें सामान्य रूप से एक ही [[इलेक्ट्रॉनिक घटक]] में निर्मित करने की आवश्यकता होती है।<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 ट्रांसप्यूटर विचारों के अवतार के रूप में था ... माइक्रोप्रोसेसरों के निर्माण के लिए जो एक दूसरे के साथ तारों के साथ | "INMOS ट्रांसप्यूटर विचारों के अवतार के रूप में था ... माइक्रोप्रोसेसरों के निर्माण के लिए जो एक दूसरे के साथ तारों के साथ संचार कर सकते थे जो उनके टर्मिनलों के बीच फैलेंगे। संस्थापक की दृष्टि थी कि सीएसपी के विचार औद्योगिक शोषण के लिए परिपक्व थे, और उन्होंने प्रोग्रामिंग ट्रांसप्यूटर्स के लिए भाषा का आधार बनाया, जिसे ओकैम (प्रोग्रामिंग भाषा) कहा जाता था। … कंपनी का अनुमान है कि इससे उन्हें एक साल पहले हार्डवेयर देने में मदद मिली, अन्यथा ऐसा नहीं होता। उन्होंने ऑक्सफोर्ड यूनिवर्सिटी कंप्यूटिंग प्रयोगशाला के संयोजन के साथ तकनीकी उपलब्धि के लिए रानी का पुरस्कार जीता और आवेदन किया। | ||
== यह भी देखें == | == यह भी देखें == | ||
| Line 207: | Line 204: | ||
* [[एडा (प्रोग्रामिंग भाषा)]] | * [[एडा (प्रोग्रामिंग भाषा)]] | ||
* [[एक्ससी प्रोग्रामिंग भाषा]] | * [[एक्ससी प्रोग्रामिंग भाषा]] | ||
* [[वेरिलॉगसीएसपी]] [[ मैक्रो (कंप्यूटर विज्ञान) ]] का एक | * [[वेरिलॉगसीएसपी]] [[ मैक्रो (कंप्यूटर विज्ञान) ]] का एक समुच्चय है जो [[वेरिलॉग एचडीएल]] में जोड़ा गया है जिससे अनुक्रमिक प्रक्रियाओं चैनल संचार संचार का समर्थन किया जा सके। | ||
* [[ जॉयस (प्रोग्रामिंग भाषा) ]] सीएसपी के सिद्धांतों पर आधारित प्रोग्रामिंग लैंग्वेज है, जिसे 1989 के आसपास [[ब्रिनच हैनसेन]] द्वारा विकसित किया गया था। | * [[ जॉयस (प्रोग्रामिंग भाषा) ]] सीएसपी के सिद्धांतों पर आधारित प्रोग्रामिंग लैंग्वेज है, जिसे 1989 के आसपास [[ब्रिनच हैनसेन]] द्वारा विकसित किया गया था। | ||
* [[सुपरपास्कल]] प्रोग्रामिंग लैंग्वेज है जिसे ब्रिन्च हैनसेन द्वारा विकसित किया गया है, जो सीएसपी और जॉयस (प्रोग्रामिंग लैंग्वेज) के साथ उनके पहले के काम से प्रभावित है। | * [[सुपरपास्कल]] प्रोग्रामिंग लैंग्वेज है जिसे ब्रिन्च हैनसेन द्वारा विकसित किया गया है, जो सीएसपी और जॉयस (प्रोग्रामिंग लैंग्वेज) के साथ उनके पहले के काम से प्रभावित है। | ||
* एडा (प्रोग्रामिंग लैंग्वेज) सीएसपी की सुविधाओं को | * एडा (प्रोग्रामिंग लैंग्वेज) सीएसपी की सुविधाओं को प्रयुक्त करता है जैसे कि मिलन स्थल। | ||
* [[डायरेक्टशो]] [[डायरेक्टएक्स]] के अंदर वीडियो ढांचा है, यह ऑडियो और वीडियो फिल्टर को | * [[डायरेक्टशो]] [[डायरेक्टएक्स]] के अंदर वीडियो ढांचा है, यह ऑडियो और वीडियो फिल्टर को प्रयुक्त करने के लिए सीएसपी अवधारणाओं का उपयोग करता है। | ||
* [[OpenCom[[RTOS]]]] औपचारिक रूप से विकसित नेटवर्क-केंद्रित वितरित RTOS है जो | * [[OpenCom[[RTOS]]]] औपचारिक रूप से विकसित नेटवर्क-केंद्रित वितरित RTOS है जो सीएसपी के व्यावहारिक सुपरसेट पर आधारित है। | ||
* इनपुट / आउटपुट ऑटोमेटन | * इनपुट / आउटपुट ऑटोमेटन | ||
* [[समानांतर प्रोग्रामिंग मॉडल]] | * [[समानांतर प्रोग्रामिंग मॉडल]] | ||
| Line 223: | Line 220: | ||
== अग्रिम पठन == | == अग्रिम पठन == | ||
* {{cite book |last=Hoare |first=C. A. R. |author-link=C. A. R. Hoare |title=Communicating Sequential Processes |orig-year=1985 |year=2004 |publisher=Prentice Hall International |url=http://www.usingcsp.com/ |isbn=978-0-13-153271-7}} | * {{cite book |last=Hoare |first=C. A. R. |author-link=C. A. R. Hoare |title=Communicating Sequential Processes |orig-year=1985 |year=2004 |publisher=Prentice Hall International |url=http://www.usingcsp.com/ |isbn=978-0-13-153271-7}} | ||
** This book has been updated by [[Jim Davies (computer scientist)|Jim Davies]] at the [[Oxford University Computing Laboratory]] and the new edition is available for download as a PDF file at the [http://www.usingcsp.com/ Using | ** This book has been updated by [[Jim Davies (computer scientist)|Jim Davies]] at the [[Oxford University Computing Laboratory]] and the new edition is available for download as a PDF file at the [http://www.usingcsp.com/ Using सीएसपी] website. | ||
* {{cite book|first=A. W.|last=Roscoe|author-link=Bill Roscoe|title=The Theory and Practice of Concurrency|publisher=[[Prentice Hall]]|isbn=978-0-13-674409-2|year=1997|url-access=registration|url=https://archive.org/details/theorypracticeof00rosc}} | * {{cite book|first=A. W.|last=Roscoe|author-link=Bill Roscoe|title=The Theory and Practice of Concurrency|publisher=[[Prentice Hall]]|isbn=978-0-13-674409-2|year=1997|url-access=registration|url=https://archive.org/details/theorypracticeof00rosc}} | ||
** Some links relating to this book are available [http://web.comlab.ox.ac.uk/oucl/publications/books/concurrency/ here]. The full text is available for download as a [http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/68b.ps PS] or [http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/68b.pdf PDF] file from Bill Roscoe's [http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/pubs.html list] of academic publications. | ** Some links relating to this book are available [http://web.comlab.ox.ac.uk/oucl/publications/books/concurrency/ here]. The full text is available for download as a [http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/68b.ps PS] or [http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/68b.pdf PDF] file from Bill Roscoe's [http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/pubs.html list] of academic publications. | ||
| Line 229: | Line 226: | ||
== बाहरी संबंध == | == बाहरी संबंध == | ||
* [http://www.usingcsp.com/ A PDF version of Hoare's | * [http://www.usingcsp.com/ A PDF version of Hoare's सीएसपी book] – Copyright restriction apply, see the page text before downloading. | ||
* [https://github.com/complex-system/Communicating-Sequential-Processes The Annotation of | * [https://github.com/complex-system/Communicating-Sequential-Processes The Annotation of सीएसपी(Chinese Version)] Non-profit translation and annotation work based on Prentice-Hall book(1985), Chaochen Zhou's Chinese Version(1988) and Jim Davies's online version(2015). | ||
* [http://www.wotug.org/ WoTUG], a User Group for | * [http://www.wotug.org/ WoTUG], a User Group for सीएसपी and occam style systems, contains some information about सीएसपी and useful links. | ||
* [http://citeseerx.ist.psu.edu/search?q=communicating+sequential+processes&submit=Search&sort=rlv&t=doc | * [http://citeseerx.ist.psu.edu/search?q=communicating+sequential+processes&submit=Search&sort=rlv&t=doc सीएसपी Citations from साइटसीर] | ||
{{Concurrent computing}} | {{Concurrent computing}} | ||
Revision as of 13:37, 22 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 अपने पर्यावरण के साथ संचार करने को तैयार है और उसके बाद a, प्रक्रिया P की तरह व्यवहार करता है .
- निर्धारक विकल्प
- नियतात्मक (या बाहरी) विकल्प संचालक प्रक्रिया के भविष्य के विकास को दो घटक प्रक्रियाओं के बीच एक विकल्प के रूप में परिभाषित करने की अनुमति देता है और पर्यावरण को किसी प्रक्रिया के लिए प्रारंभिक घटना को संप्रेषित करके विकल्प को हल करने की अनुमति देता है। उदाहरण के लिए, वह प्रक्रिया है जो प्रारंभिक घटनाओं a और b को संप्रेषित करने के लिए तैयार है और बाद में या तो P या Q,के रूप व्यवहार करता है जिसके आधार पर पर्यावरण संचार करने के लिए प्रारंभिक घटना का चयन करता है। यदि दोनों a और b को एक साथ संप्रेषित किया गया था, तो विकल्प को गैर-निर्धारित रूप से हल किया जाएगा।
- गैर नियतात्मक विकल्प
- गैर नियतात्मक (या आंतरिक) विकल्प संचालक प्रक्रिया के भविष्य के विकास को दो घटक प्रक्रियाओं के बीच विकल्प के रूप में परिभाषित करने की अनुमति देता है, किन्तु पर्यावरण को किसी भी नियंत्रण की अनुमति नहीं देता है कि कौन से घटक प्रक्रियाओं का चयन किया जाएगा। उदाहरण के लिए, जैसा व्यवहार कर सकता है या . मानने से इंकार कर सकता है a या b और संचार करने के लिए तभी बाध्य है जब पर्यावरण दोनों प्रदान करता है a और b. यदि विकल्प के दोनों पक्षों की प्रारंभिक घटनाएँ समान हैं, तो गैर-नियतात्मकता को अनजाने में नाममात्र निर्धारक विकल्प में प्रस्तुत किया जा सकता है। तो, उदाहरण के लिए,
- या तो या की तरह व्यवहार कर सकता है। यह a या b को स्वीकार करने से इंकार कर सकता है और केवल तभी संचार करने के लिए बाध्य होता है | जब पर्यावरण a और b दोनों प्रदान करता है। यदि विकल्प के दोनों पक्षों की प्रारंभिक घटनाएँ समान हैं, तो गैर-नियतात्मकता को अनजाने में एक नाममात्र नियतात्मक विकल्प में प्रस्तुत किया जा सकता है। तो उदाहरण के लिएके समान है |
- इंटरलिविंग
- इंटरलीविंग संचालक पूरी तरह से स्वतंत्र समवर्ती गतिविधि का प्रतिनिधित्व करता है। प्रक्रिया दोनों के रूप में व्यवहार करता है P और Q इसके साथ ही। दोनों प्रक्रियाओं की घटनाओं को इच्छानुसार समय के साथ जोड़ा जाता है।
- इंटरफ़ेस समानांतर
- इंटरफ़ेस समानांतर संचालक समवर्ती गतिविधि का प्रतिनिधित्व करता है जिसके लिए घटक प्रक्रियाओं के बीच सिंक्रनाइज़ेशन की आवश्यकता होती है: इंटरफ़ेस समुच्चय में कोई भी घटना तभी हो सकती है जब सभी घटक प्रक्रियाएँ उस घटना में संलग्न होने में सक्षम हों। उदाहरण के लिए, प्रक्रिया P और Q दोनों की तरह एक साथ व्यवहार करता है। दोनों प्रक्रियाओं a की घटनाओं को इच्छानुसार समय के साथ जोड़ा जाता है।कार्य a में सम्मिलित हो सकते हैं और प्रक्रिया बन सकते हैं |जबकिबस गतिरोध होगा।
- प्रच्छादन
- प्रच्छादन वाला संचालक कुछ घटनाओं को अप्राप्य बनाकर सार प्रक्रियाओं की विधि प्रदान करता है। प्रच्छादन का सामान्य उदाहरण है | जो यह मानते हुए कि P में प्रकट नहीं होने वाली घटना a को कम कर देता है |
उदाहरण
मूलरूप सीएसपी उदाहरणों में से चॉकलेट वेंडिंग मशीन का एक सार प्रतिनिधित्व है और कुछ चॉकलेट खरीदने के इच्छुक व्यक्ति के साथ इसकी परस्पर क्रिया है। यह वेंडिंग मशीन दो अलग-अलग घटनाओं, "कॉइन" और "चोक" को अंजाम देने में सक्षम हो सकती है | जो क्रमशः भुगतान की प्रविष्टि और चॉकलेट की डिलीवरी का प्रतिनिधित्व करती हैं। एक मशीन जो चॉकलेट देने से पहले भुगतान (केवल नकद में) की मांग करती है, उसे इस प्रकार लिखा जा सकता है |
एक व्यक्ति जो भुगतान करने के लिए सिक्के या कार्ड का उपयोग करना चुन सकता है | उसे इस प्रकार मॉडल किया जा सकता है |
इन दोनों प्रक्रियाओं को समानांतर में रखा जा सकता है | जिससे वे दूसरे के साथ परस्पर क्रिया कर सकें। समग्र प्रक्रिया का व्यवहार उन घटनाओं पर निर्भर करता है | जिन पर दो घटक प्रक्रियाओं को सिंक्रनाइज़ करना चाहिए। इस प्रकार,
जबकि यदि केवल "कॉइन" पर सिंक्रोनाइज़ेशन की आवश्यकता होती है, तो हम प्राप्त करेंगे
यदि हम "सिक्का" और "कार्ड" घटनाओं को छिपाकर इस बाद की समग्र प्रक्रिया को सार करते हैं, अर्थात
हमें गैर-नियतात्मक प्रक्रिया मिलती है |
यह ऐसी प्रक्रिया है जो या तो "चोक" घटना की प्रस्तुति करती है और फिर रुक जाती है, या बस रुक जाती है। दूसरे शब्दों में, यदि हम अमूर्तता को प्रणाली के बाहरी दृश्य के रूप में मानते हैं (उदाहरण के लिए, कोई व्यक्ति जो व्यक्ति द्वारा किए गए निर्णय को नहीं देखता है), गैर-नियतात्मक एल्गोरिदम प्रस्तुत किया गया है।
औपचारिक परिभाषा
वाक्य - विन्यास
सीएसपी का वाक्य - विन्यास "नियमबद्ध" विधियों को परिभाषित करता है | जिसमें प्रक्रियाओं और घटनाओं को जोड़ा जा सकता है। माना e एक घटना हो, और X घटनाओं का समुच्चय हो। तब सीएसपी के मूल वाक्य - विन्यास को इस प्रकार परिभाषित किया जा सकता है |
ध्यान दें कि, संक्षिप्तता के हित में, ऊपर प्रस्तुत वाक्य - विन्यास प्रक्रिया को छोड़ देता है, जो विचलन (कंप्यूटर विज्ञान) के साथ-साथ विभिन्न ऑपरेटरों जैसे वर्णानुक्रमिक समानांतर पाइपिंग और अनुक्रमित विकल्पों का प्रतिनिधित्व करता है।
औपचारिक शब्दार्थ
सीएसपी को कई अलग-अलग अर्थ विज्ञान कंप्यूटर विज्ञान से ओत-प्रोत किया गया है | जो वाक्यगत रूप से सही सीएसपी अभिव्यक्तियों के अर्थ को परिभाषित करता है। सीएसपी के सिद्धांत में पारस्परिक रूप से सुसंगत शब्दार्थ शब्दार्थ, बीजगणितीय शब्दार्थ (कंप्यूटर विज्ञान), और परिचालन शब्दार्थ सम्मिलित हैं।
सांकेतिक शब्दार्थ
सीएसपी के तीन प्रमुख सांकेतिक मॉडल ट्रेस मॉडल, स्थिर विफलता मॉडल और विफलता/विचलन मॉडल हैं। इन तीन मॉडलों में से प्रत्येक के लिए प्रक्रिया अभिव्यक्तियों से अर्थ मैपिंग सीएसपी के लिए अर्थ संबंधी शब्दार्थ प्रदान करते हैं।[1]
निशान मॉडल प्रक्रिया अभिव्यक्ति के अर्थ को घटनाओं (निशान) के अनुक्रमों के समुच्चय के रूप में परिभाषित करता है | जिसे प्रदर्शन करने के लिए प्रक्रिया देखी जा सकती है। उदाहरण के लिए,
- तब से कोई कार्य नहीं करता है |
- प्रक्रिया के बाद से यह देखा जा सकता है कि कोई घटना नहीं हुई है, घटना a, या घटनाओं का क्रम a के बाद b का प्रदर्शन नहीं किया है
अधिक औपचारिक रूप से, ट्रेसेस मॉडल में प्रक्रिया का अर्थ P के रूप में परिभाषित किया गया है | ऐसा है कि:
- (अर्थात। खाली अनुक्रम सम्मिलित है)
- (अर्थात। उपसर्ग-बंद है)
जहाँ घटनाओं के सभी संभावित परिमित अनुक्रमों का समुच्चय है।
स्थिर विफलता मॉडल इनकार करने वाले समुच्चय के साथ निशान मॉडल का विस्तार करता है, जो घटनाओं के समुच्चय हैं कि प्रक्रिया प्रदर्शन करने से इंकार कर सकती है। एक जोड़ी है , एक निशान से मिलकर s, और इनकार समुच्चय X जो उन घटनाओं की पहचान करता है | जो ट्रेस को निष्पादित करने के बाद एक प्रक्रिया से इनकार कर सकती हैं | s स्थिर विफलता मॉडल में एक प्रक्रिया के देखे गए व्यवहार को जोड़ी द्वारा वर्णित किया गया है | उदाहरण के लिए,
विफलताओं / विचलन मॉडल आगे विचलन (कंप्यूटर विज्ञान) को संभालने के लिए विफलताओं के मॉडल का विस्तार करता है। विफलताओं/विचलन मॉडल में एक प्रक्रिया का शब्दार्थ एक जोड़ी है जहाँ सभी निशानों के समुच्चय के रूप में परिभाषित किया गया है जो अलग-अलग व्यवहार और जन्म दे सकता है |
उपकरण
वर्षों से, सीएसपी का उपयोग करके वर्णित प्रणालियों के विश्लेषण और समझने के लिए कई उपकरण तैयार किए गए हैं। प्रारंभिक उपकरण कार्यान्वयन ने सीएसपी के लिए विभिन्न प्रकार के मशीन-पठनीय वाक्य - विन्यास का उपयोग किया, जिससे विभिन्न उपकरणों के लिए लिखी गई इनपुट फाइलें असंगत हो गईं। हालाँकि, अधिकांश सीएसपी उपकरण अब ब्रायन स्कैटरगूड द्वारा तैयार की गई सीएसपी की मशीन-पठनीय बोली पर मानकीकृत हो गए हैं, जिसे कभी-कभी सीएसपी के रूप में संदर्भित किया जाता है।M.[18] सीएसपीM सीएसपी की बोली में औपचारिक रूप से परिभाषित परिचालन शब्दार्थ है, जिसमें एम्बेडेड कार्यात्मक प्रोग्रामिंग भाषा सम्मिलित है।
सबसे प्रसिद्ध सीएसपी उपकरण शायद फेल्योर/डाइवर्जेंस रिफाइनमेंट 2 (एफडीआर2) है, जो फॉर्मल सिस्टम्स (यूरोप) लिमिटेड द्वारा विकसित वाणिज्यिक उत्पाद है। एफडीआर2 को अक्सर मॉडल चेकर के रूप में वर्णित किया जाता है, किन्तु तकनीकी रूप से इसमें एक शोधन जांचकर्ता है। यह दो सीएसपी प्रक्रिया अभिव्यक्तियों को लेबल किए गए संक्रमण प्रणाली (एलटीएस) में परिवर्तित करता है, और फिर यह निर्धारित करता है कि प्रक्रियाओं में से कुछ निर्दिष्ट सिमेंटिक मॉडल (निशान, विफलताओं, या विफलताओं/विचलन) के भीतर दूसरे का परिशोधन है या नहीं।[19] FDR2 राज्य-स्थान के आकार को कम करने के लिए एलटीएस प्रक्रिया के लिए विभिन्न राज्य-स्थान संपीड़न एल्गोरिदम प्रयुक्त करता है जिसे शोधन जांच के समय खोजा जाना चाहिए। FDR2 को FDR3 द्वारा सफल किया गया है, पूरी तरह से फिर से लिखा गया संस्करण है जिसमें समानांतर निष्पादन और एकीकृत प्रकार चेकर सम्मिलित है। यह ऑक्सफोर्ड विश्वविद्यालय द्वारा जारी किया गया है, जिसने 2008-12 की अवधि में FDR2 भी जारी किया था।[20] एडिलेड शोधन परीक्षक (एआरसी)[21] एडीलेड विश्वविद्यालय में औपचारिक मॉडलिंग और सत्यापन समूह द्वारा विकसित सीएसपी शोधन परीक्षक है। ARC, FDR2 से इस मायने में भिन्न है कि यह आंतरिक रूप से सीएसपी प्रक्रियाओं को द्विआधारी निर्णय आरेख (OBDDs) के रूप में प्रस्तुत करता है, जो राज्य-अंतरिक्ष संपीड़न एल्गोरिदम जैसे कि FDR2 में उपयोग किए जाने वाले एल्गोरिदम के उपयोग की आवश्यकता के बिना स्पष्ट LTS अभ्यावेदन की राज्य विस्फोट समस्या को कम करता है।
प्रोबी परियोजना,[22] जिसे Institut für Informatik, Heinrich-Heine-Universität Düsseldorf द्वारा होस्ट किया जाता है, मूल रूप से B विधि में निर्मित विनिर्देशों के विश्लेषण का समर्थन करने के लिए बनाया गया था। चूँकि, इसमें परिशोधन जांच और रैखिक लौकिक तर्क मॉडल-जांच दोनों के माध्यम से सीएसपी प्रक्रियाओं के विश्लेषण के लिए समर्थन भी सम्मिलित है। ProB का उपयोग संयुक्त सीएसपी और B विनिर्देशों के गुणों को सत्यापित करने के लिए भी किया जा सकता है। एक ProBE सीएसपी एनिमेटर FDR3 में एकीकृत है।
प्रक्रिया विश्लेषण टूलकिट (पीएटी)
[23][24] सिंगापुर के राष्ट्रीय विश्वविद्यालय में स्कूल ऑफ कंप्यूटिंग में विकसित सीएसपी विश्लेषण उपकरण है। पीएटी परिशोधन जांच, एलटीएल मॉडल-जांच, और सीएसपी और समयबद्ध सीएसपी प्रक्रियाओं का अनुकरण करने में सक्षम है। PAT प्रोसेस लैंग्वेज सीएसपी को म्यूटेबल शेयर्ड वेरिएबल्स, एसिंक्रोनस मैसेज पासिंग, और विभिन्न प्रकार की निष्पक्षता और मात्रात्मक समय से संबंधित प्रक्रिया निर्माणों के समर्थन के साथ विस्तारित करती है जैसे कि deadline और waituntil. पीएटी प्रक्रिया भाषा का अंतर्निहित रचना सिद्धांत प्रक्रियात्मक कार्यक्रमों के साथ एक उच्च स्तरीय विनिर्देश भाषा को जोड़ना है (उदाहरण के लिए पीएटी में घटना अनुक्रमिक कार्यक्रम या यहां तक कि बाहरी सी # पुस्तकालय कॉल भी हो सकती है) अधिक अभिव्यक्ति के लिए। परिवर्तनीय साझा चर और अतुल्यकालिक चैनल मानक सीएसपी में उपयोग किए जाने वाले प्रसिद्ध प्रक्रिया मॉडलिंग पैटर्न के लिए सुविधाजनक सिंटैक्टिक चीनी प्रदान करते हैं। पीएटी वाक्य - विन्यास समान है, किन्तु सीएसपी के समान नहीं हैM.[25] पीएटी वाक्य - विन्यास और मानक सीएसपी के बीच मुख्य अंतरM प्रक्रिया अभिव्यक्तियों को समाप्त करने के लिए अर्धविरामों का उपयोग, चर और असाइनमेंट के लिए सिंटैक्टिक चीनी को सम्मिलित करना, और आंतरिक विकल्प और समांतर संरचना के लिए थोड़ा अलग वाक्यविन्यास का उपयोग करना है।
विजुअलनेट्स[26] विनिर्देशों से सीएसपी प्रणाली के एनिमेटेड विज़ुअलाइज़ेशन का उत्पादन करता है, और समयबद्ध सीएसपी का समर्थन करता है। Capsim[27] आलसी सिम्युलेटर है। यह सीएसपी की जांच मॉडल नहीं करता है, किन्तु बहुत बड़ी (संभावित रूप से अनंत) प्रणालियों की खोज के लिए उपयोगी है।
SyncStitch इंटरैक्टिव मॉडलिंग और पर्यावरण विश्लेषण के साथ एक सीएसपी शोधन परीक्षक है। इसमें ग्राफिकल स्टेट-ट्रांज़िशन डायग्राम एडिटर है। उपयोगकर्ता प्रक्रियाओं के व्यवहार को न केवल सीएसपी अभिव्यक्तियों बल्कि राज्य-संक्रमण आरेखों के रूप में मॉडल कर सकता है। जाँच के परिणाम को ग्राफ़िक रूप से कम्प्यूटेशन-ट्री के रूप में भी रिपोर्ट किया जाता है और परिधीय निरीक्षण उपकरणों के साथ अंतःक्रियात्मक रूप से विश्लेषण किया जा सकता है। परिशोधन जांच के अलावा, यह डेडलॉक जांच और लाइवलॉक जांच भी कर सकता है।
संबंधित औपचारिकताएं
कई अन्य विनिर्देशन भाषाएं और औपचारिकताएं क्लासिक असमय सीएसपी से, या उससे प्रेरित होकर प्राप्त की गई हैं, जिनमें सम्मिलित हैं:
- समयबद्ध सीएसपी, जिसमें रीयल-टाइम प्रणाली के बारे में तर्क करने के लिए समय संबंधी जानकारी सम्मिलित है
- रिसेप्टिव प्रोसेस थ्योरी, सीएसपी की विशेषज्ञता जो एसिंक्रोनस (यानी गैर-अवरुद्ध एल्गोरिदम ) सेंड ऑपरेशन मानती है
- CSPP
- एचसीएसपी
- TCOZ, समयबद्ध सीएसपी और ऑब्जेक्ट जेड का एकीकरण
- Circus, प्रोग्रामिंग के एकीकृत सिद्धांतों पर आधारित सीएसपी और Z विनिर्देश भाषा का एकीकरण
- सीएमएल Archived 2020-02-19 at the Wayback Machine (कम्पास मॉडलिंग लैंग्वेज), Circus और VDM विनिर्देश भाषा का संयोजन विकसित किया गया है। प्रणाली की प्रणाली (एसओएस) की मॉडलिंग
- CspCASL, सामान्य बीजगणितीय विशिष्टता भाषा का विस्तार जो एकीकृत करता है सीएसपी
टेम्पोरल ऑर्डरिंग विशिष्टता की भाषा भाषा, अंतरराष्ट्रीय मानक[28] जिसमें सीएसपी और कम्युनिकेटिंग सिस्टम्स की कैलकुलस की विशेषताएँ सम्मिलित हैं।
- PALPS, अन्ना फिलिपो द्वारा विकसित पारिस्थितिक मॉडल के लिए स्थानों के साथ संभावित विस्तार और Mauricio toro bermúdez [es]
अभिनेता मॉडल के साथ तुलना
जहाँ तक यह संदेशों का आदान-प्रदान करने वाली समवर्ती प्रक्रियाओं से संबंधित है, अभिनेता मॉडल मोटे तौर पर सीएसपी के समान है। हालाँकि, दो मॉडल उनके द्वारा प्रदान किए जाने वाले प्राचीन के संबंध में कुछ मूलभूत रूप से भिन्न विकल्प बनाते हैं:
- सीएसपी प्रक्रियाएं गुमनाम होती हैं, जबकि अभिनेताओं की पहचान होती है।
- सीएसपी संदेश भेजने के लिए स्पष्ट चैनलों का उपयोग करता है, जबकि अभिनेता प्रणाली नामित गंतव्य अभिनेताओं को संदेश प्रेषित करते हैं। इन दृष्टिकोणों को एक दूसरे का दोहरा माना जा सकता है, इस अर्थ में कि चैनल के माध्यम से प्राप्त होने वाली प्रक्रियाओं की प्रभावी रूप से उस चैनल के अनुरूप पहचान होती है, जबकि अभिनेताओं के बीच नाम-आधारित युग्मन को चैनलों के रूप में व्यवहार करने वाले अभिनेताओं का निर्माण करके तोड़ा जा सकता है।
- सीएसपी संदेश-पासिंग में मूल रूप से संदेश भेजने और प्राप्त करने में सम्मिलित प्रक्रियाओं के बीच एक मेल मिलाप सम्मिलित है, यानी प्रेषक तब तक संदेश प्रेषित नहीं कर सकता जब तक कि रिसीवर इसे स्वीकार करने के लिए तैयार न हो। इसके विपरीत, अभिनेता प्रणालियों में संदेश-पासिंग मौलिक रूप से अतुल्यकालिक है, यानी संदेश संचरण और स्वागत एक ही समय में नहीं होता है, और प्रेषक संदेशों को प्राप्त करने से पहले उन्हें स्वीकार करने के लिए तैयार कर सकते हैं। इन दृष्टिकोणों को एक दूसरे के दोहरे भी माना जा सकता है, इस अर्थ में कि मिलन-स्थल-आधारित प्रणालियों का उपयोग बफ़र संचार के निर्माण के लिए किया जा सकता है जो अतुल्यकालिक संदेश प्रणाली के रूप में व्यवहार करता है, जबकि अतुल्यकालिक प्रणालियों का उपयोग संदेश/ पावती प्रोटोकॉल प्रेषकों और रिसीवरों को सिंक्रनाइज़ करने के लिए।
ध्यान दें कि उपरोक्त गुण होरे द्वारा मूल सीएसपी पेपर को जरूरी नहीं बताते हैं, बल्कि गोलंग और क्लोजर के कोर एसिंक्रोनस जैसे कार्यान्वयन में देखा गया विचार का आधुनिक अवतार है। मूल कागज में, चैनल विनिर्देश का केंद्रीय भाग नहीं थे, और प्रेषक और रिसीवर प्रक्रियाएं वास्तव में एक दूसरे को नाम से पहचानती हैं।
पुरस्कार
1990 में, "तकनीकी उपलब्धि के लिए एलिज़ाबेथ द्वितीय का पुरस्कार ... ऑक्सफोर्ड यूनिवर्सिटी कंप्यूटिंग प्रयोगशाला में प्रदान किया गया है। [ऑक्सफोर्ड यूनिवर्सिटी] कंप्यूटिंग प्रयोगशाला। यह पुरस्कार प्रयोगशाला और इनमोस लिमिटेड के बीच सफल सहयोग को मान्यता देता है। ... इनमोस का प्रमुख उत्पाद 'ट्रांसप्यूटर' है, माइक्रोप्रोसेसर जिसमें कई पुर्जे होते हैं जिन्हें सामान्य रूप से एक ही इलेक्ट्रॉनिक घटक में निर्मित करने की आवश्यकता होती है।[29] टोनी होरे के अनुसार,[30] "INMOS ट्रांसप्यूटर विचारों के अवतार के रूप में था ... माइक्रोप्रोसेसरों के निर्माण के लिए जो एक दूसरे के साथ तारों के साथ संचार कर सकते थे जो उनके टर्मिनलों के बीच फैलेंगे। संस्थापक की दृष्टि थी कि सीएसपी के विचार औद्योगिक शोषण के लिए परिपक्व थे, और उन्होंने प्रोग्रामिंग ट्रांसप्यूटर्स के लिए भाषा का आधार बनाया, जिसे ओकैम (प्रोग्रामिंग भाषा) कहा जाता था। … कंपनी का अनुमान है कि इससे उन्हें एक साल पहले हार्डवेयर देने में मदद मिली, अन्यथा ऐसा नहीं होता। उन्होंने ऑक्सफोर्ड यूनिवर्सिटी कंप्यूटिंग प्रयोगशाला के संयोजन के साथ तकनीकी उपलब्धि के लिए रानी का पुरस्कार जीता और आवेदन किया।
यह भी देखें
- ट्रेस सिद्धांत, निशान का सामान्य सिद्धांत।
- ट्रेस मोनोइड और इतिहास मोनोइड
- एडा (प्रोग्रामिंग भाषा)
- एक्ससी प्रोग्रामिंग भाषा
- वेरिलॉगसीएसपी मैक्रो (कंप्यूटर विज्ञान) का एक समुच्चय है जो वेरिलॉग एचडीएल में जोड़ा गया है जिससे अनुक्रमिक प्रक्रियाओं चैनल संचार संचार का समर्थन किया जा सके।
- जॉयस (प्रोग्रामिंग भाषा) सीएसपी के सिद्धांतों पर आधारित प्रोग्रामिंग लैंग्वेज है, जिसे 1989 के आसपास ब्रिनच हैनसेन द्वारा विकसित किया गया था।
- सुपरपास्कल प्रोग्रामिंग लैंग्वेज है जिसे ब्रिन्च हैनसेन द्वारा विकसित किया गया है, जो सीएसपी और जॉयस (प्रोग्रामिंग लैंग्वेज) के साथ उनके पहले के काम से प्रभावित है।
- एडा (प्रोग्रामिंग लैंग्वेज) सीएसपी की सुविधाओं को प्रयुक्त करता है जैसे कि मिलन स्थल।
- डायरेक्टशो डायरेक्टएक्स के अंदर वीडियो ढांचा है, यह ऑडियो और वीडियो फिल्टर को प्रयुक्त करने के लिए सीएसपी अवधारणाओं का उपयोग करता है।
- [[OpenComRTOS]] औपचारिक रूप से विकसित नेटवर्क-केंद्रित वितरित RTOS है जो सीएसपी के व्यावहारिक सुपरसेट पर आधारित है।
- इनपुट / आउटपुट ऑटोमेटन
- समानांतर प्रोग्रामिंग मॉडल
- TLA+ समवर्ती प्रणालियों के मॉडलिंग और सत्यापन के लिए अन्य औपचारिक भाषा है।
संदर्भ
- ↑ 1.0 1.1 1.2 1.3 Roscoe, A. W. (1997). समरूपता का सिद्धांत और अभ्यास (PDF). Prentice Hall. ISBN 978-0-13-674409-2.
- ↑ Inmos (1995-05-12). occam 2.1 Reference Manual (PDF). SGS-THOMSON Microelectronics Ltd., INMOS document 72 occ 45 03.
- ↑ 3.0 3.1 Cox, Russ. "बेल लैब्स और सीएसपी थ्रेड्स". Retrieved 2010-04-15.
- ↑ "10 अकादमिक और ऐतिहासिक प्रश्न". Retrieved 2021-11-15.
- ↑ "FAQ: Why build concurrency on the ideas of CSP?". The Go Programming Language. Retrieved 2021-10-15.
- ↑ Hickey, Rich (2013-06-28). "क्लोजर कोर.एसिंक चैनल". Retrieved 2021-10-15.
- ↑ 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.
- ↑ Abdallah, Ali E.; Jones, Cliff B.; Sanders, Jeff W. (2005). Communicating Sequential Processes: The First 25 Years. LNCS. Vol. 3525. Springer. ISBN 9783540258131.
- ↑ 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.
- ↑ 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.
- ↑ Creese, S. (2001). Data Independent Induction: CSP Model Checking of Arbitrary Sized Networks (D. Phil.). Oxford University. CiteSeerX 10.1.1.13.7185.
- ↑ 12.0 12.1 Hoare, C. A. R. (1985). अनुक्रमिक प्रक्रियाओं का संचार करना. Prentice Hall. ISBN 978-0-13-153289-2.
- ↑ Clinger, William (June 1981). अभिनेता शब्दार्थ की नींव (Mathematics Doctoral Dissertation). MIT. hdl:1721.1/6935.
- ↑ 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.
- ↑ 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.
- ↑ 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.
- ↑ 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.
- ↑ Scattergood, J.B. (1998). "मशीन-पठनीय सीएसपी का शब्दार्थ और कार्यान्वयन". D.Phil. Oxford University Computing Laboratory.
{{cite journal}}: Cite journal requires|journal=(help) - ↑ 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) - ↑ "Introduction — FDR 4.2.4 documentation". www.cs.ox.ac.uk.
- ↑ 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.
- ↑ 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.
- ↑ 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.
- ↑ 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.
- ↑ 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.
- ↑ Green, Mark; Abdallah, Ali (2002). "संचार प्रणालियों के अनुकूलन के लिए प्रदर्शन विश्लेषण और व्यवहार ट्यूनिंग". Communicating Process Architectures 2002.
- ↑ Brooke, Phillip; Paige, Richard (2007). "सीएसपीसिम के साथ आलसी अन्वेषण और सीएसपी मॉडल की जांच". Communicating Process Architectures 2007.
- ↑ ISO 8807, Language of Temporal Ordering Specification
- ↑ Geraint Jones (1990). "Sharp as a Razor: A Queen's Award for the Computing Laboratory". The Oxford Magazine (59, Fourth Week, Trinity Term).
- ↑ Len Shustek (March 2009). "C.A.R के साथ एक साक्षात्कार होरे". Communications of the ACM. 52 (3): 38–41. doi:10.1145/1467247.1467261. S2CID 1868477.
अग्रिम पठन
- Hoare, C. A. R. (2004) [1985]. Communicating Sequential Processes. Prentice Hall International. ISBN 978-0-13-153271-7.
- This book has been updated by Jim Davies at the Oxford University Computing Laboratory and the new edition is available for download as a PDF file at the Using सीएसपी website.
- Roscoe, A. W. (1997). The Theory and Practice of Concurrency. Prentice Hall. ISBN 978-0-13-674409-2.
बाहरी संबंध
- A PDF version of Hoare's सीएसपी book – Copyright restriction apply, see the page text before downloading.
- The Annotation of सीएसपी(Chinese Version) Non-profit translation and annotation work based on Prentice-Hall book(1985), Chaochen Zhou's Chinese Version(1988) and Jim Davies's online version(2015).
- WoTUG, a User Group for सीएसपी and occam style systems, contains some information about सीएसपी and useful links.
- सीएसपी Citations from साइटसीर
| General | |
|---|---|
| Process calculi | |
| Classic problems | |
