العمليات التسلسلية المتواصلة (نموذج حوسبة)

في علوم الكمبيوتر ، تُعتبر **عمليات الاتصال المتسلسلة (CSP)** لغة صورية تستخدم لوصف أنماط التفاعل في الأنظمة المتزامنة. وهي تنتمي إلى مجموعة النظريات الرياضية للتزامن المعروفة باسم **جبر العمليات** أو **حساب العمليات**، التي تعتمد أساسًا على تبادل الرسائل عبر القنوات.

وقد كان لنموذج CSP تأثير بالغ الأهمية في تصميم لغة البرمجة **أوكام**. كما ألهم تصميم العديد من لغات البرمجة الأخرى مثل **[[ليمبو (لغة برمجة)|ليمبو]]**، و **RaftLib**، و **[[إرلانج]]**، و **[[غو (لغة برمجة)|غو]]** ، و **[[كريستال (لغة برمجة)|كريستال]]**، بالإضافة إلى مكتبة **core.async** في لغة **[[كلوجر (لغة برمجة)|كلوجر]]**.

أُورِدَ وصف نموذج **عمليات الاتصال المتسلسلة (CSP)** للمرة الأولى على يد '''توني هوار''' في مقال نُشر عام 1978، وشهد تطورات جوهرية منذ ذلك الحين. وقد استُخدم CSP على نطاق تطبيقي واسع في الصناعة كأداة لتوصيف والتحقق من الجوانب المتزامنة في طيف متنوع من الأنظمة، من بينها معالج **T9000 Transputer**، بالإضافة إلى أنظمة التجارة الإلكترونية الآمنة. إن نظرية الطاقة الشمسية المركزة نفسها لا تزال أيضًا موضوعًا للبحث النشط، بما في ذلك العمل على زيادة نطاق تطبيقها العملي (على سبيل المثال، زيادة نطاق الأنظمة التي يمكن تحليلها بسهولة). 

## تاريخ

### النسخة الأصلية
كانت النسخة الأولى من CSP، التي قدمها **هوار** في مقاله عام 1978، أقرب إلى لغة برمجة متزامنة بدائية وليست حساب عمليات بالمعنى الدقيق. تميزت بناء جملة مختلفة بشكل كبير عن الإصدارات اللاحقة من CSP، وافتقرت إلى دلالات محددة رياضيًا، كما لم تكن قادرة على تمثيل عدم التحديد غير المحدود. في CSP الأصلي، كانت البرامج تُكتب كتكوين متوازٍ لعدد ثابت من العمليات المتسلسلة التي تتواصل فيما بينها حصريًا عبر تبادل الرسائل المتزامنة.على النقيض من الإصدارات اللاحقة من CSP، تم تعيين اسم صريح لكل عملية، وتم تحديد مصدر أو وجهة الرسالة من خلال تحديد اسم عملية الإرسال أو الاستلام المقصودة. على سبيل المثال، العملية
 نسخ = *[c:character; غرب؟ ج → شرق! ج]
يشير مصطلح "التكوين المتوازي" إلى طريقة دمج أو تجميع عدة عمليات لتكوين نظام أكبر. في سياق CSP، يتم تمثيل التكوين المتوازي لعمليتين، على سبيل المثال P و Q، بالرمز $\(P \parallel Q\)$. هذا يعني أن العمليتين P و Q تعملان بشكل متزامن وتتفاعلان مع بعضهما البعض عبر قنوات الاتصال.
 [غرب: تفكيك || X: نسخ || شرق: تجميع]
تقوم هذه العبارة بتحديد أسماء لثلاث عمليات مختلفة ثم تنفذها بشكل متزامن. 

### التطوير في جبر العمليات
بعد نشر النسخة الأصلية من CSP، قام هواري وستيفن بروكس وأيه دبليو روسكوي بتطوير وتحسين *نظرية* CSP إلى شكلها الجبري العملي الحديث. كان النهج المتبع في تطوير CSP إلى جبر العملية متأثرًا بعمل روبن ميلنر في حساب أنظمة الاتصال (CCS) والعكس صحيح. تم تقديم النسخة النظرية من CSP في البداية في مقال عام 1984 بقلم بروكس وهوار وروسكو،  وفي وقت لاحق في كتاب هوار *"التواصل بالعمليات المتسلسلة"* ،  والذي نُشر في عام 1985. في سبتمبر 2006، كان هذا الكتاب لا يزال ثالث أكثر المراجع استشهادًا في علوم الكمبيوتر على الإطلاق وفقًا لـ Citeseer (على الرغم من أن المصدر المذكور قد لا يكون موثوقًا به تمامًا نظرًا لطبيعة العينة التي استُخلص منها). لقد طرأت بعض التعديلات الطفيفة على نظرية CSP منذ نشر كتاب **هوار**. وكان الدافع الرئيسي وراء معظم هذه التغييرات هو ظهور أدوات آلية تهدف إلى تحليل نماذج CSP والتحقق من صحتها. ويقدم كتاب **Roscoe** المعنون "نظرية وممارسة التزامن" وصفًا لهذا الإصدار الأحدث من CSP.

### التطبيقات
كان أحد التطبيقات المبكرة والهامة لنموذج **عمليات الاتصال المتسلسلة (CSP)** هو استخدامه في تحديد والتحقق من عناصر معالج **INMOS T9000 Transputer**. كان T9000 معالجًا دقيقًا فائق القياس ومعقدًا صُمم لدعم المعالجة المتعددة على نطاق واسع. وقد استُخدم CSP في التحقق من صحة كل من خط أنابيب المعالج ووحدة معالجة القنوات الافتراضية، التي كانت مسؤولة عن إدارة الاتصالات خارج شريحة المعالج.

عادةً ما ركزت التطبيقات الصناعية لنموذج **عمليات الاتصال المتسلسلة (CSP)** في تصميم البرمجيات على الأنظمة التي تتطلب موثوقية عالية وحساسة للسلامة. على سبيل المثال، قام **معهد بريمن للأنظمة الآمنة** وشركة **دايملر بنز للفضاء** بوضع نموذج لنظام إدارة الأخطاء وواجهة إلكترونيات الطيران (الذي يتكون من حوالي 23000 سطر من التعليمات البرمجية) والمخصص للاستخدام في **محطة الفضاء الدولية** باستخدام CSP. وقد قاموا بتحليل هذا النموذج للتأكد من أن تصميمهم خالٍ من حالات الجمود (deadlock) والحبس الحي (livelock) .   تمكنت عملية النمذجة والتحليل من الكشف عن عدد من الأخطاء التي كان من الصعب اكتشافها باستخدام الاختبار وحده. وعلى نحو مماثل، طبقت شركة Praxis High Integrity Systems نمذجة وتحليل CSP أثناء تطوير البرمجيات (حوالي 100 ألف سطر من التعليمات البرمجية) لهيئة إصدار شهادات بطاقات ذكية آمنة للتحقق من أن تصميمها آمن وخالٍ من الجمود. تزعم شركة براكسيس أن النظام لديه معدل عيوب أقل بكثير من الأنظمة المماثلة. 

نظرًا لأن نموذج **عمليات الاتصال المتسلسلة (CSP)** يتمتع بقدرة فائقة على نمذجة وتحليل الأنظمة التي تتضمن تبادلات رسائل معقدة، فقد تم تطبيقه أيضًا على نطاق واسع للتحقق من صحة بروتوكولات الاتصالات والأمان. ومن الأمثلة البارزة على هذا النوع من التطبيقات استخدام **Lowe** لنموذج CSP واستخدام مدقق التحسين **FDR** لاكتشاف هجوم غير معروف سابقًا عل بروتوكول مصادقة المفتاح العام Needham–Schroeder ، ثم تطوير بروتوكول مصحح قادر على هزيمة الهجوم. 

## وصف غير رسمي
كما يوحي اسمه، يتيح نموذج **عمليات الاتصال المتسلسلة (CSP)** وصف الأنظمة من منظور مكونات مستقلة تعمل كعمليات، ولا تتفاعل مع بعضها البعض إلا عبر قنوات الاتصال التي تنقل الرسائل. ومع ذلك، فإن الجزء "المتسلسل" من اسم CSP يُعتبر الآن تسمية غير دقيقة إلى حد ما. يسمح CSP الحديث بتعريف العمليات المكونة ليس فقط كعمليات متسلسلة، بل أيضًا كتكوين متوازٍ لعمليات أكثر أساسية. يتم وصف العلاقات بين العمليات المختلفة، والطريقة التي تتواصل بها كل عملية مع بيئتها، باستخدام مشغلات جبرية مختلفة للعمليات . وباستخدام هذا النهج الجبري، يمكن بسهولة إنشاء أوصاف معقدة للغاية للعمليات من عدد قليل من العناصر البدائية.

### البدائيون
يوفر نموذج **عمليات الاتصال المتسلسلة (CSP)** فئتين أساسيتين من العناصر الأولية في جبر العمليات الخاص به: **الأحداث** و **العمليات البدائية**.
الأحداث
تمثل **الأحداث** في CSP عمليات الاتصال أو التفاعل بين العمليات وبيئتها أو بين العمليات المتزامنة ذاتها. وتتميز بكونها فورية، حيث أن الملاحظة الخارجية للعملية تقتصر على هذه الاتصالات. لا يقع الحدث إلا بتوافق البيئة، وإذا عرضت العملية حدثًا وكانت البيئة مستعدة، فيجب أن يحدث. ويمكن أن تكون الأحداث مجرد أسماء ذرية بسيطة. (مثل  و  )، أو أسماء مركبة (مثل  و  )، أو أحداث إدخال/إخراج (مثل  و  ). مجموعة كل الأحداث يشار إليها \Sigma . 

; العمليات البدائية

تجسد **العمليات البدائية** في CSP السلوكيات الأساسية التي تُستخدم كنقطة انطلاق لبناء وصف أكثر تعقيدًا للأنظمة المتزامنة. من الأمثلة على هذه العمليات الأولية: STOP، التي تمثل حالة التوقف الفوري أو الانسداد، و SKIP، التي تعبر عن الإكمال الناجح والفوري للعملية.

### العمليات الجبرية
يشتمل نموذج **عمليات الاتصال المتسلسلة (CSP)** على مجموعة واسعة من **المُشغلات الجبرية** (Algebraic Operators). وفيما يلي عرض غير رسمي للعناصر الرئيسية من هذه المشغلات

; بادئة

يقوم **عامل البادئة** (Prefix Operator) بدمج حدث وعملية لإنتاج عملية جديدة. على سبيل المثال، العملية a \to P هي عملية تبدأ بالرغبة في التواصل مع بيئتها عبر الحدث a. وبعد وقوع الحدث a، تتصرف العملية الجديدة تمامًا مثل العملية (P).

; التكرار

يُمكن تعريف العمليات في CSP باستخدام مفهوم **التكرار**. فإذا كان F(P) يمثل أي تعبير في CSP يتضمن العملية P، فإن \mu P. F(P) يُعرّف عملية متكررة تحقق المعادلة \mu P. F(P). وبالمثل، يمكن تعريف التكرارات بشكل تبادلي.مثل


\begin{align}
& P_u = up \to P_d\\
& P_d = down \to P_u\\
\end{align}
 الذي يحدد زوجًا من العمليات المتكررة المتبادلة التي تتناوب بين التواصل up و down . 

; الاختيار الحتمي

يُمكِّن **مشغل الاختيار الحتمي (deterministic choice)**، ويُعرف أيضًا باسم **الاختيار الخارجي (external choice)**، من تحديد المسار المستقبلي لتطور عملية ما كخيار بين عمليتين فرعيتين. في هذا النوع من الاختيار، تلعب البيئة دورًا حاسمًا في تحديد أي من العمليتين سيتم تنفيذهما لاحقًا، وذلك عن طريق التواصل مع حدث أولي خاص بإحدى العمليتين.، (a \to P)\ \Box\ (b \to Q) هي العملية التي ترغب في توصيل الأحداث الأولية a و b ويتصرف بعد ذلك كأي منهما P أو Q ، اعتمادًا على الحدث الأولي الذي تختار البيئة التواصل معه. 

; الاختيار غير الحتمي

يمكّن **مشغل الاختيار غير الحتمي (nondeterministic choice)**، ويُعرف أيضًا باسم **الاختيار الداخلي (internal choice)**، من تحديد المسار المستقبلي لتطور عملية ما كبديل بين عمليتين فرعيتين، ولكن دون منح البيئة أي قدرة على التأثير أو التحكم في أي من هاتين العمليتين سيتم اختيارهما للتنفيذ. على سبيل المثال (a \to P) \sqcap (b \to Q) يمكن أن يتصرف مثل أي منهما a \to P أو b \to Q . ويمكنه أن يرفض القبول a أو b ولا يلتزم بالتواصل إلا إذا كانت البيئة توفر كليهما a و b .يمكن أن ينشأ **عدم التحديد** بشكل غير مقصود في عملية اختيار حتمي اسميًا ($\(\square\)$) إذا كانت الأحداث الأولية التي يمكن أن تحدث في كلا جانبي الاختيار متطابقة.(a \to a \to \mathrm{STOP})\ \Box\ (a \to b \to \mathrm{STOP}) و a \to \big((a \to \mathrm{STOP}) \sqcap (b \to \mathrm{STOP})\big) متكافئة. 

; التداخل

يمثل **عامل التداخل** (Interleaving Operator) تنفيذًا متزامنًا ومستقلاً تمامًا لعمليتين. العملية P \;|||\; Q تتصرف كسلوك كل من العملية P والعملية Q في آن واحد. تتداخل الأحداث الصادرة من كلتا العمليتين بترتيب عشوائي في الزمن.

يمكن أن يؤدي التداخل إلى إدخال **عدم التحديد** حتى لو كانت كل من P و Q عمليتين حتميتين في حد ذاتهما. فإذا كان بإمكان كل من $\(P\)$ و Q التواصل عبر نفس الحدث، فإن العملية P \;|||\; Q ستختار بشكل غير حتمي أي من العمليتين قامت بتوصيل هذا الحدث في تلك اللحظة.

; واجهة متوازية

يجسد **عامل التوازي في الواجهة** (أو التوازي المعمم) نشاطًا متزامنًا يتطلب تنسيقًا أو تزامنًا بين العمليات المكونة. P \;|[X]|\; Q ، أي حدث في مجموعة الواجهة X \subseteq \Sigma لا يمكن لهذا الحدث أن يقع إلا بتوافر شرط مشاركة كل من P و Q فيه.

على سبيل المثال، العملية P \;|[\{ a \}]|\; Q تتطلب أن يكون كل منP و Q قادرين على تنفيذ الحدث a حتى يقع هذا الحدث. بناءً على ذلك، فإن العملية. لذا، فإن العملية (a \to P) \;|[\{ a \}]|\; (a \to Q) يعادل a \to (P \;|[\{ a \}]|\; Q) ، بينما (a \to P ) \;|[\{ a, b \}]|\; (b \to Q) يعادل \mathrm{STOP} (أي حالة تصل فيها العملية إلى طريق مسدود ولا يمكنها التقدم أكثر).

; إخفاء

يوفر **عامل الإخفاء** (Hiding Operator) في CSP طريقة قوية لتجريد العمليات من التفاصيل الداخلية، وذلك عن طريق جعل مجموعة معينة من الأحداث غير قابلة للملاحظة أو غير مرئية للبيئة الخارجية. P \setminus X هي العملية P مع مجموعة الحدث X مختفي.

مثال بسيط على استخدام عامل الإخفاء هو (a \to P) \setminus \{ a \}. وبافتراض أن الحدث a لا يظهر في العملية P، فإن هذه العملية تختزل ببساطة إلى العملية P.

يتم استيعاب الأحداث المخفية على هيئة أفعال داخلية غير مرئية وغير قابلة للتحكم من قبل البيئة، ويُشار إليها عادةً بالرمز (\mu P. a \to P) \setminus \{ a \}. يؤدي وجود عامل الإخفاء إلى إدخال سلوك إضافي يُعرف باسم **التباعد (<math>\mathbf{div}</math>)**.

### أمثلة
أحد الأمثلة الكلاسيكية للتفاعلات الرقمية هو التمثيل المجرد لآلة بيع الشوكولاتة وتفاعلاتها مع شخص يرغب في شراء قطعة من الشوكولاتة. قد تكون هذه الآلة قادرة على تنفيذ حدثين متميزين: "**عملة**" (يمثل إدخال الدفع) و "**شوكولاتة**" (يمثل تسليم الشوكولاتة). يمكن وصف سلوك الآلة التي تتطلب إدخال الدفع (بالنقود فقط) قبل تقديم الشوكولاتة على النحو التالي باستخدام لغة CSP:

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

يمكن نمذجة سلوك شخص قد يختار استخدام عملة معدنية أو بطاقة لإجراء عملية دفع على النحو التالي في لغة CSP:

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

هذه العملية إما أن تقدم حدثًا باسم "شوكولاتة" ثم تتوقف عن العمل، أو أنها تتوقف مباشرة دون تقديم أي حدث. وبعبارة أخرى، إذا نظرنا إلى التجريد على أنه رؤية خارجية للنظام (على سبيل المثال، من منظور شخص لا يرى عملية اتخاذ القرار الداخلي)، فإن هذا يمثل حالة من  **(nondeterminism)**.

## التعريف الرسمي

### بناء الجملة
يحدد بناء جملة لغة CSP الطرق "القياسية" التي يمكن بها تجميع العمليات والأحداث. لنفترض أن e يمثل حدثًا ما، وأن X يمثل مجموعة من الأحداث. عندئذٍ، يمكن تعريف البناء الأساسي لجملة لغة CSP على النحو التالي:


\begin{array}{lcll}
{Proc} & ::= & \mathrm{STOP} & \; \\
&|& \mathrm{SKIP} & \; \\
&|& e \rightarrow {Proc} & (\text{prefixing})\\
&|& {Proc} \;\Box\; {Proc} & (\text{external} \; \text{choice})\\
&|& {Proc} \;\sqcap\; {Proc} & (\text{nondeterministic} \; \text{choice})\\
&|& {Proc} \;\vert\vert\vert\; {Proc} & (\text{interleaving}) \\
&|& {Proc} \;|[ \{ X \} ]| \;{Proc} & (\text{interface} \; \text{parallel})\\
&|& {Proc} \setminus X & (\text{hiding})\\
&|& {Proc} ; {Proc} & (\text{sequential} \; \text{composition})\\
&|& \mathrm{if} \; b \; \mathrm{then} \; {Proc}\; \mathrm{else}\; Proc & (\text{boolean} \; \text{conditional})\\
&|& {Proc} \;\triangleright\; {Proc} & (\text{timeout})\\
&|& {Proc} \;\triangle\; {Proc} & (\text{interrupt})
\end{array}


تجدر الإشارة إلى أنه بغرض الإيجاز، فإن البناء النحوي الموضح أعلاه يحذف عامل "**div**" الذي يمثل التباعد، بالإضافة إلى العديد من العوامل الأخرى مثل الاختيارات المتوازية الأبجدية، وعامل الأنابيب (piping)، والاختيارات المفهرسة.

### الدلالات الرسمية
تتضمن لغة CSP مجموعة متنوعة من '''الدلالات الرسمية''' المختلفة، والتي تحدد المعنى الدقيق للتعبيرات الصحيحة نحويًا في لغة CSP. تشمل النظرية الكامنة وراء CSP  المتسقة المتبادلة، و  ، و الدلالات التشغيلية

### الدلالات الإشارية
تتمثل النماذج الدلالية الرئيسية الثلاثة للغة CSP في **نموذج التتبعات (Traces Model)**، و **نموذج الفشل المستقر (Stable Failures Model)**، و **نموذج الفشل/التباعدات (Failures/Divergences Model)**. وتوفر التعيينات الدلالية من تعبيرات العملية إلى كل من هذه النماذج الثلاثة الدلالات الرسمية للغة CSP .

#### نموذج الآثار
يُعرّف **نموذج التتبعات** معنى تعبير العملية على أنه مجموعة من تسلسلات الأحداث (التتبعات) التي يمكن ملاحظتها أثناء قيام العملية بتنفيذها. على سبيل المثال،

* \mathrm{traces}\left(\mathrm{STOP}\right) = \left\{ \langle\rangle \right\} منذ \mathrm{STOP} لا يقوم بأي أحداث
* \mathrm{traces}\left(a\rightarrow b \rightarrow \mathrm{STOP}\right) = \left\{\langle\rangle ,\langle a \rangle, \langle a, b \rangle \right\} منذ العملية (a\rightarrow b \rightarrow \mathrm{STOP}) يمكن ملاحظة عدم حدوث أي أحداث، أو الحدث  ، أو تسلسل الأحداث  الذي يليه 

بشكل أكثر دقة، يُعرّف **نموذج الآثار** \mathcal T بأنه مجموعة من المجموعات الفرعية المغلقة ذات البادئة غير الفارغة للمجموعة \Sigma^{\ast} (مجموعة جميع التسلسلات المنتهية المحتملة للأحداث من الأبجدية Σ). ويُحدد معنى العملية  في نموذج الآثار على أنه مجموعة من الآثار \mathrm{traces}\left(P\right) \subseteq \Sigma^{\ast} بحيث:

# \langle\rangle \in \mathrm{traces}\left(P\right) (أي \mathrm{traces}\left(P\right) يحتوي على التسلسل الفارغ)
# s_1 \smallfrown s_2 \in \mathrm{traces}\left(P\right) \implies s_1 \in \mathrm{traces}\left(P\right) (أي \mathrm{traces}\left(P\right) (مغلقة بالبادئة)

أين \Sigma^{\ast} هي مجموعة كل التسلسلات المحدودة الممكنة للأحداث.

#### نموذج الفشل المستقر
يمتد **نموذج الفشل المستقر** إلى **نموذج التتبعات** باستخدام **مجموعات الرفض**، وهي مجموعات من الأحداث X⊆Σ التي يمكن للعملية أن ترفض القيام بها. يُعرّف **الفشل** بأنه زوج (s,X)، يتكون من تتبع s ومجموعة رفض X تحدد الأحداث التي قد ترفض العملية المشاركة فيها بمجرد تنفيذ التتبع s. ويُوصَف السلوك المرصود لعملية في نموذج الفشل المستقر بواسطة الزوج (traces(P),failures(P))، حيث

\left(\mathrm{traces}\left(P\right), \mathrm{failures}\left(P\right)\right) . على سبيل المثال،

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

#### نموذج الفشل/التباعد
ويمتد **نموذج الفشل/التباعد** إلى **نموذج الفشل** لمعالجة حالات التباعد بشكل منفصل. وتُعرّف دلالات العملية في نموذج الفشل/التباعد على أنها زوج\left(\mathrm{failures}_\perp\left(P\right), \mathrm{divergences}\left(P\right)\right) أين \mathrm{divergences}\left(P\right) **تُعرّف على أنها مجموعة كل الآثار التي يمكن أن تؤدي إلى سلوك متباعد و** \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\} .

#### نقاط ثابتة فريدة
أحد المبادئ الأساسية في لغة CSP هو **قاعدة النقطة الثابتة الفريدة (Unique Fixed Point Rule - UFP)**. تنص إحدى الصيغ الخاصة بالتكرارات الفردية في نموذج التتبعات على أنه إذا F : \mathcal T \rightarrow \mathcal T هي دالة على مجموعات التتبع التي تم إنشاؤها بواسطة عملية **التكرار المحمي**، X ، و Y هي عملية حيث \mathrm{traces}(Y) هي نقطة ثابتة لـ F ، ثم X يعادل Y في نموذج الآثار . ويمكن أيضًا توسيع قاعدة النقطة الثابتة الفريدة (UFP) لتشمل التكرارات المتبادلة ونماذج CSP الأخرى.

## أدوات
على مدار السنوات، تم تطوير العديد من الأدوات لتحليل وفهم الأنظمة التي يتم وصفها باستخدام لغة CSP. استخدمت التطبيقات الأولية لهذه الأدوات مجموعة متنوعة من القواعد النحوية التي يمكن قراءتها آليًا لـ CSP، مما أدى إلى عدم توافق ملفات الإدخال المكتوبة لأدوات مختلفة. ومع ذلك، فقد اتجهت غالبية أدوات CSP الآن نحو التوحيد القياسي على لهجة CSP التي يمكن قراءتها آليًا والتي ابتكرها برايان سكاترجود.والتي يشار إليها أحيانًا باسم CSP *M.*  تتمتع لهجة CSP *M* من CSP بدلالات تشغيلية محددة رسميًا، والتي تتضمن لغة برمجة وظيفية مضمنة.

### روزفلت
ربما تكون الأداة الأكثر شيوعًا لتحليل لغة CSP هي Failures-Divergences Refinement (FDR)، وهو منتج تجاري تم تطويره في الأصل بواسطة شركة Formal Systems (Europe) Ltd. غالبًا ما يوصف FDR بأنه مدقق نموذج (model checker)، ولكنه من الناحية التقنية مدقق تحسين (refinement checker). يقوم FDR بتحويل تعبيرين لعملية CSP إلى أنظمة انتقال مُصنفة (Labeled Transition Systems - LTS)، ثم يحدد ما إذا كانت إحدى العمليتين تمثل تحسينًا للأخرى ضمن نموذج دلالي محدد (سواء كان ذلك نموذج الآثار، أو نموذج الإخفاقات، أو نموذج الإخفاقات/التباعد).  تطبق FDR خوارزميات ضغط مختلفة لمساحة الحالة على عمليات LTS من أجل تقليل حجم مساحة الحالة التي يجب استكشافها أثناء فحص التحسين. خلف FDR FDR2 وFDR3 وFDR4. 

### قوس
**مدقق تحسين أديلايد (ARC)**  هو أداة لفحص وتحسين نماذج CSP، وقد تم تطويرها بواسطة مجموعة النمذجة والتحقق الرسمية في جامعة أديلايد. يتميز ARC عن مدقق FDR2 في طريقة تمثيله الداخلية لعمليات CSP، حيث يستخدم **مخططات قرار ثنائية مرتبة (OBDDs)**. يساهم هذا النهج في التخفيف من مشكلة انفجار الحالات التي تواجه التمثيلات الصريحة لأنظمة انتقال الحالة (LTS)، وذلك دون الحاجة إلى استخدام خوارزميات ضغط مساحة الحالة المشابهة لتلك المستخدمة في FDR2.

### بروب
تم تطوير مشروع **ProB** ، الذي يستضيفه معهد المعلوماتية بجامعة هاينريش هاينه في دوسلدورف، في الأساس لدعم تحليل المواصفات المكتوبة بلغة B. ومع ذلك، فقد تم توسيع قدراته ليشمل دعم تحليل عمليات CSP من خلال إجراء فحوصات التحسين والتحقق من نماذج LTL (المنطق الزمني الخطي). بالإضافة إلى ذلك، يمكن استخدام ProB للتحقق من خصائص المواصفات التي تجمع بين لغتي CSP و B. وقد تم دمج برنامج **ProBE CSP Animator** الخاص بالمشروع في أداة FDR3.

### بات
*مجموعة أدوات تحليل العملية* (PAT)   هي أداة تحليل CSP تم تطويرها في كلية الحوسبة في الجامعة الوطنية في سنغافورة . تتمكن PAT من إجراء فحص التحسين، وفحص نموذج LTL، ومحاكاة عمليات CSP وCSP المؤقتة. تمتد لغة عملية PAT إلى CSP مع دعم للمتغيرات المشتركة القابلة للتغيير، وتمرير الرسائل غير المتزامنة، ومجموعة متنوعة من هياكل العملية المتعلقة بالعدالة والوقت الكمي مثل `deadline` و `waituntil` . المبدأ الأساسي لتصميم لغة عملية PAT هو الجمع بين لغة المواصفات عالية المستوى والبرامج الإجرائية (على سبيل المثال، قد يكون الحدث في PAT عبارة عن برنامج متسلسل أو حتى استدعاء مكتبة C# خارجية) لتحقيق قدر أكبر من التعبيرية. توفر المتغيرات المشتركة القابلة للتغيير والقنوات غير المتزامنة بنية نحوية مبسطة ومريحة لأنماط نمذجة العمليات الشائعة المستخدمة في لغة CSP القياسية. يتميز بناء جملة لغة PAT بتشابه مع لغة CSP *M*، ولكنه ليس مطابقًا لها تمامًا . وتتمثل الاختلافات الرئيسية بين بناء جملة PAT ولغة CSP *M* القياسية في استخدام الفواصل المنقوطة لإنهاء تعبيرات العمليات، وإضافة بنية نحوية مختصرة للمتغيرات والمهام، واستخدام صيغة مختلفة قليلًا لعمليات الاختيار الداخلي والتكوين المتوازي.

### آحرون
يقوم برنامج VisualNets بإنشاء تصورات متحركة لأنظمة CSP انطلاقًا من مواصفاتها، كما يدعم لغة CSP الموقوتة زمنيًا.

يُعد برنامج  CSPsim محاكيًا يعتمد على التقييم الكسول (Lazy evaluation). وعلى الرغم من أنه لا يجري عملية فحص شاملة لنموذج CSP، إلا أنه يظل أداة قيمة لاستكشاف الأنظمة الكبيرة جدًا، والتي قد تكون ذات طبيعة لانهائية.

SyncStitch هي أداة متخصصة في فحص وتحسين نماذج CSP، وتوفر بيئة تفاعلية للنمذجة والتحليل. تتضمن الأداة محررًا رسوميًا لإنشاء مخططات انتقال الحالة. يتيح ذلك للمستخدم نمذجة سلوك العمليات ليس فقط باستخدام تعبيرات CSP النصية، بل أيضًا من خلال تمثيلها بصريًا كرسم بياني لانتقال الحالة. ويتم عرض نتائج عملية الفحص بيانيًا على شكل أشجار حسابية، مما يسهل تحليلها بشكل تفاعلي باستخدام أدوات فحص مخصصة. بالإضافة إلى فحوصات التحسين، تدعم SyncStitch إجراء فحوصات للكشف عن حالات الجمود وحالات الإغلاق المباشر.

## الصياغات ذات الصلة
انبثقت أو استُلهمت العديد من لغات المواصفات والصيغ الرسمية الأخرى من لغة CSP الكلاسيكية غير المحددة زمنيًا، ومن بينها:

* CSP الموقوت ، والذي يتضمن معلومات التوقيت للتفكير في أنظمة الوقت الفعلي
* نظرية العملية الاستقبالية ، وهي تخصص من CSP يفترض عملية إرسال غير متزامنة (أي غير حاجب )
* سي إس بي بي
* برنامج خدمات الرعاية الصحية المجتمعية
* TCOZ ، وهو تكامل بين Timed CSP و Object Z
* السيرك ، وهو عبارة عن دمج بين CSP و Z استنادًا إلى نظريات البرمجة الموحدة
*  CML (لغة نمذجة COMPASS)، وهي مزيج من Circus و VDM تم تطويرها لنمذجة أنظمة الأنظمة (SoS)
* CspCASL ، وهو امتداد لـ CASL يدمج CSP
* LOTOS ، وهو معيار دولي يتضمن ميزات CSP و CCS .
* PALPS ، وهو امتداد احتمالي مع مواقع للنماذج البيئية التي طورها آنا فيليبو وموريسيو تورو بيرموديز

## مقارنة مع نموذج الممثل
في سياق الأنظمة المتزامنة التي تعتمد على تبادل الرسائل، يتقارب نموذج الممثل بشكل ملحوظ مع نموذج CSP. ومع ذلك، يتبنى النموذجان خيارات مختلفة جوهريًا فيما يتعلق بالعناصر الأولية التي يقدمونها:

* عمليات CSP مجهولة الهوية، في حين أن الجهات الفاعلة لها هويات.
* يستخدم CSP قنوات صريحة لتمرير الرسائل، بينما ترسل أنظمة الجهات الفاعلة الرسائل إلى الجهات الفاعلة الوجهة المسماة. يمكن اعتبار هذه الأساليب ثنائية لبعضها البعض، بمعنى أن العمليات التي تستقبل من خلال قناة واحدة لها هوية تتوافق فعليًا مع تلك القناة، في حين يمكن كسر الاقتران القائم على الاسم بين الجهات الفاعلة من خلال بناء جهات فاعلة تتصرف كقنوات.
* يتضمن تمرير الرسائل CSP بشكل أساسي التقاء بين العمليات المشاركة في إرسال واستقبال الرسالة، أي أن المرسل لا يستطيع إرسال رسالة حتى يكون المستقبل جاهزًا لقبولها. على النقيض من ذلك، فإن نقل الرسائل في أنظمة الجهات الفاعلة هو أمر غير متزامن بشكل أساسي، أي أن إرسال الرسائل واستقبالها ليس من الضروري أن يحدث في نفس الوقت، وقد يرسل المرسلون الرسائل قبل أن يكون المستلمون مستعدين لقبولها. يمكن أيضًا اعتبار هذه الأساليب ثنائية لبعضها البعض، بمعنى أنه يمكن استخدام الأنظمة القائمة على الالتقاء لبناء اتصالات مؤقتة تتصرف كأنظمة مراسلة غير متزامنة، بينما يمكن استخدام الأنظمة غير المتزامنة لبناء اتصالات على غرار الالتقاء باستخدام بروتوكول الرسالة/الإقرار لمزامنة المرسلين والمستقبلين.

إن السمات المذكورة سابقًا لا تعكس بالضرورة التصور الأولي لـ CSP كما قدمه Hoare في ورقته البحثية الأصلية. بل إنها تمثل الفهم والتطبيق الحديثين لهذه الأفكار، كما هو واضح في تطبيقات مثل لغة Go ومكتبة core.async في لغة Clojure. ففي النسخة الأصلية من CSP، لم تكن القنوات مكونًا محوريًا في المواصفات، وكانت عمليات الإرسال والاستقبال تعتمد على تحديد الطرف الآخر بالاسم لإتمام الاتصال.

## جائزة
في عام 1990، مُنح **مختبر الحوسبة بجامعة [[أكسفورد]]** **جائزة الملكة للإنجاز التكنولوجي**. وقد جاء هذا التكريم اعترافًا بالشراكة المثمرة التي جمعت المختبر بشركة Inmos Ltd. وكان المنتج الأساسي لشركة Inmos هو "**transputer**"، وهو عبارة عن معالج دقيق يدمج في مكون واحد العديد من الأجزاء التي عادةً ما تكون مطلوبة بشكل منفصل.  وفقًا لتوني هوار،  "كان INMOS Transputer تجسيدًا لأفكار ... بناء معالجات دقيقة يمكنها التواصل مع بعضها البعض عبر أسلاك تمتد بين محطاتها. كان لدى المؤسس رؤية مفادها أن أفكار **CSP** كانت ناضجة للاستغلال الصناعي، وجعل ذلك أساس لغة برمجة Transputer، والتي كانت تسمى Occam . ... قدرت الشركة أنها مكنتهم من تسليم الأجهزة قبل عام واحد مما كان سيحدث بخلاف ذلك. تقدموا بطلب وفازوا بجائزة الملكة للإنجاز التكنولوجي، بالاشتراك مع مختبر الحوسبة بجامعة أكسفورد."

## انظر أيضا

* نظرية الأثر ، النظرية العامة للآثار.
* تتبع المونويد والتاريخ المونويد
* لغة البرمجة السهلة
* لغة برمجة XC
* VerilogCSP عبارة عن مجموعة من وحدات الماكرو المضافة إلى Verilog HDL لدعم عمليات الاتصال المتسلسلة عبر قنوات الاتصالات.
* Joyce هي لغة برمجة تعتمد على مبادئ CSP، تم تطويرها بواسطة Brinch Hansen حوالي عام 1989.
* SuperPascal هي لغة برمجة طورها أيضًا Brinch Hansen ، متأثرًا بـ CSP وعمله السابق مع Joyce .
* تطبق Ada ميزات CSP مثل اللقاء.
* DirectShow هو إطار عمل الفيديو داخل DirectX ، ويستخدم مفاهيم CSP لتنفيذ مرشحات الصوت والفيديو.
* OpenComRTOS هو نظام تشغيل في الوقت الحقيقي موزع يتمحور حول الشبكة وتم تطويره رسميًا ويعتمد على مجموعة فرعية عملية من CSP.
* أتمتة الإدخال/الإخراج
* نموذج البرمجة المتوازية
* TLA+ هي لغة رسمية أخرى للنمذجة والتحقق من الأنظمة المتزامنة.

## مراجع

## قراءة إضافية

* 
** 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 CSP'' website.
* 
** Some links relating to this book are available here. The full text is available for download as a PS or PDF file from Bill Roscoe's list of academic publications.

## روابط خارجية

* نسخة PDF من كتاب Hoare's CSP - تخضع لقيود حقوق النشر، راجع نص الصفحة قبل التنزيل.
* ''شرح CSP'' (النسخة الصينية) ، عمل ترجمة وشرح غير ربحي يعتمد على كتاب برنتيس هول (1985)، والنسخة الصينية لتشاوتشين تشو (1988)، والنسخة الإلكترونية لجيم ديفيز (2015).
* تحتوي WoTUG ، وهي مجموعة مستخدمين لأنظمة CSP وأسلوب أوكام، على بعض المعلومات حول CSP والروابط المفيدة.
* "استشهادات CSP" من ''CiteSeer''

تصنيف:حوسبة متزامنة
تصنيف:علم الحاسوب في 1978
تصنيف:استحداثات متعلقة بالحواسيب في 1978