التواصل بشأن العمليات المتسلسلة

كانت نسخة CSP المُقدَّمة في مقالة هوار الأصلية عام 1978 لغة برمجة متزامنة في جوهرها، وليست حسابًا للعمليات . كان لها بناء جملة مختلف تمامًا عن الإصدارات اللاحقة من CSP، ولم تكن تمتلك دلالات مُحدَّدة رياضيًا، ^{[ 12 ]} ولم تكن قادرة على تمثيل عدم الحتمية غير المحدودة . ^{[ 13 ]} كُتِبت البرامج في CSP الأصلية كتركيب متوازٍ لعدد ثابت من العمليات المتسلسلة التي تتواصل فيما بينها حصريًا من خلال تمرير الرسائل المتزامن. على عكس الإصدارات اللاحقة من CSP، كان لكل عملية اسم صريح، وكان مصدر الرسالة أو وجهتها يُحدَّد بتحديد اسم عملية الإرسال أو الاستقبال المقصودة. على سبيل المثال، العملية

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

يستقبل بشكل متكرر حرفًا من العملية المسماة westويرسل ذلك الحرف إلى العملية المسماة east. التركيب المتوازي

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

^{[ 7 ]} يُعيّن الأسماء westللعملية DISASSEMBLE، Xوللعملية COPY، eastوللعملية ASSEMBLE، وينفذ هذه العمليات الثلاث في وقت واحد.

بعد نشر النسخة الأصلية من نظرية العمليات المتسلسلة المتصلة (CSP)، قام كل من هوار وستيفن بروكس وإيه دبليو روسكو بتطويرها وتحسينها إلى شكلها الجبري الحديث القائم على العمليات. وقد تأثر النهج المتبع في تطوير CSP إلى جبر العمليات بعمل روبن ميلنر في حساب الأنظمة المتصلة (CCS)، والعكس صحيح. عُرضت النسخة النظرية من CSP مبدئيًا في مقال نُشر عام 1984 من قِبل بروكس وهوار وروسكو ^{[ 14 ]} ، ثم لاحقًا في كتاب هوار " العمليات المتسلسلة المتصلة" ^[ 12 ^{] الذي} نُشر عام 1985. في سبتمبر 2006، كان هذا الكتاب لا يزال ثالث أكثر المراجع استشهادًا في علوم الحاسوب على الإطلاق وفقًا لموقع Citeseer (مع العلم أنه مصدر غير موثوق به نظرًا لطبيعة عينة البيانات التي يعتمدها). وقد شهدت نظرية CSP بعض التغييرات الطفيفة منذ نشر كتاب هوار. كانت معظم هذه التغييرات مدفوعة بظهور أدوات مؤتمتة لتحليل عمليات CSP والتحقق منها. ويصف كتاب روسكو " نظرية وممارسة التزامن" ^{[ 1 ]} هذا الإصدار الأحدث من CSP.

كان من أوائل التطبيقات المهمة لتقنية CSP استخدامها في تحديد مواصفات عناصر معالج INMOS T9000 Transputer والتحقق منها ، وهو معالج معقد فائق القياس ذو بنية خطية مصمم لدعم المعالجة المتعددة واسعة النطاق . استُخدمت تقنية CSP للتحقق من صحة كل من خط أنابيب المعالج ومعالج القناة الافتراضية ، الذي كان يدير الاتصالات الخارجية للمعالج. ^{[ 9 ]}

عادةً ما تركز التطبيقات الصناعية لمنهجية CSP في تصميم البرمجيات على الأنظمة الموثوقة والحساسة للسلامة. فعلى سبيل المثال، قام معهد بريمن للأنظمة الآمنة وشركة دايملر-بنز للفضاء بنمذجة نظام إدارة الأعطال وواجهة إلكترونيات الطيران (يتكون من حوالي 23000 سطر برمجي) المُخصص للاستخدام في محطة الفضاء الدولية باستخدام منهجية CSP، ثم قاموا بتحليل النموذج للتأكد من خلو تصميمهم من حالات التعطل التام والتعطل الجزئي . ^{[ 15 ] [ 16 ]} وقد كشفت عملية النمذجة والتحليل عن عدد من الأخطاء التي كان من الصعب اكتشافها باستخدام الاختبار وحده. وبالمثل، طبقت شركة براكسيس للأنظمة عالية الموثوقية نمذجة وتحليل CSP أثناء تطوير برنامج (يتكون من حوالي 100000 سطر برمجي) لهيئة اعتماد بطاقات ذكية آمنة للتحقق من أمان تصميمها وخلوه من حالات التعطل التام. وتدعي براكسيس أن النظام يتميز بمعدل عيوب أقل بكثير من الأنظمة المماثلة. ^{[ 10 ]}

نظرًا لأن CSP مناسب تمامًا لنمذجة وتحليل الأنظمة التي تتضمن تبادلات رسائل معقدة، فقد تم تطبيقه أيضًا على التحقق من بروتوكولات الاتصالات والأمان. ومن الأمثلة البارزة على هذا النوع من التطبيقات استخدام لوي لـ CSP ومدقق تحسين FDR لاكتشاف هجوم غير معروف سابقًا على بروتوكول مصادقة المفتاح العام نيدهام-شرودر ، ثم تطوير بروتوكول مصحح قادر على صد الهجوم. ^{[ 17 ]}

يوفر CSP فئتين من العناصر الأولية في جبر العمليات الخاص به: الأحداث والعمليات الأولية.

الفعاليات

تمثل الأحداث الاتصالات أو التفاعلات. يُفترض أنها فورية، واتصالها هو كل ما يمكن أن تعرفه "البيئة" الخارجية عن العمليات. لا يتم إرسال الحدث إلا إذا سمحت البيئة بذلك. إذا قدمت عملية ما حدثًا وسمحت البيئة بذلك، فيجب إرسال هذا الحدث. قد تكون الأحداث أسماءً ذرية (مثل: تشغيل ، إيقاف )، أو أسماءً مركبة (مثل: valve.open ، valve.close )، أو أحداث إدخال/إخراج (مثل: mouse?xy ، screen!bitmap ). يُرمز إلى مجموعة جميع الأحداث بـ${\displaystyle \Sigma }$[ ^{18 ]​}

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

تمثل العمليات الأولية سلوكيات أساسية: ومن الأمثلة على ذلك${\displaystyle \mathrm {توقف} }$(العملية التي تؤدي إلى حالة جمود فورية)، و${\displaystyle \mathrm {SKIP} }$(العملية التي تنتهي بنجاح على الفور). ^{[ 18 ]}

تحتوي لغة CSP على مجموعة واسعة من المؤثرات الجبرية. ويمكن تلخيص أهمها بشكل غير رسمي كما يلي.

بادئة

يجمع عامل البادئة بين حدث وعملية لإنتاج عملية جديدة. على سبيل المثال،${\displaystyle a\to P}$هي العملية التي ترغب في التواصل بشأن الحدث${\displaystyle a}$مع بيئتها، وبعد ذلك${\displaystyle a}$، يتصرف مثل العملية${\displaystyle P}$[ ^{18 ]​}

التكرار

يمكن تعريف العمليات باستخدام الاستدعاء الذاتي. حيث${\displaystyle F(P)}$أي مصطلح من مصطلحات مزودي خدمات الحوسبة السحابية يتضمن${\displaystyle P}$العملية${\displaystyle \mu PF(P)}$يُعرّف عملية تكرارية معطاة بالمعادلة ${\displaystyle P=F(P)}$يمكن أيضًا تعريف العلاقات التكرارية بشكل متبادل، مثل: $${\displaystyle {\begin{aligned}&P_{u}=up\to P_{d}\\&P_{d}=down\to P_{u}\\\end{aligned}}}$$ وهو ما يُعرّف زوجًا من العمليات المتكررة المتبادلة التي تتناوب بين التواصل${\displaystyle up}$و${\displaystyle down}$[ ^{18 ]​}

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

يُتيح عامل الاختيار الحتمي (أو الخارجي) تحديد التطور المستقبلي لعملية ما على أنه اختيار بين عمليتين مكونتين، كما يُتيح للبيئة حسم هذا الاختيار من خلال إرسال حدث أولي لإحدى العمليتين. على سبيل المثال،${\displaystyle (a\to P)\ \Box \ (b\to Q)}$هي العملية التي ترغب في إبلاغ الأحداث الأولية${\displaystyle a}$و${\displaystyle b}$ويتصرف لاحقاً إما${\displaystyle P}$أو${\displaystyle Q}$، وذلك بحسب الحدث الأولي الذي تختاره البيئة للتواصل. ^{[ 18 ]}

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

يُتيح عامل الاختيار غير الحتمي (أو الداخلي) تحديد التطور المستقبلي لعملية ما على أنه اختيار بين عمليتين مكونتين، ولكنه لا يمنح البيئة أي سيطرة على أي من العمليتين المكونتين سيتم اختيارها. على سبيل المثال،${\displaystyle (a\to P)\sqcap (b\to Q)}$يمكن أن يتصرف مثل أي منهما${\displaystyle a\to P}$أو${\displaystyle b\to Q}$يمكنها رفض القبول${\displaystyle a}$أو${\displaystyle b}$ولا يكون ملزماً بالتواصل إلا إذا كانت البيئة توفر كلا الأمرين${\displaystyle a}$و${\displaystyle b}$.

قد يُدخَل عدم الحتمية دون قصد إلى خيار يبدو ظاهريًا حتميًا إذا كانت الأحداث الأولية لكلا طرفي الخيار متطابقة. على سبيل المثال، $${\displaystyle (a\to a\to \mathrm {STOP} )\ \Box \ (a\to b\to \mathrm {STOP} )}$$و $${\displaystyle a\to {\big (}(a\to \mathrm {STOP} )\sqcap (b\to \mathrm {STOP} ){\big )}}$$ متكافئان. ^{[ 18 ]}

التداخل

يمثل عامل التداخل نشاطًا متزامنًا مستقلًا تمامًا. العملية${\displaystyle P\;|||\;Q}$يتصرف على كلا الجانبين${\displaystyle P}$و${\displaystyle Q}$في آن واحد. تتداخل أحداث العمليتين بشكل عشوائي في الزمن. يمكن أن يؤدي التداخل إلى عدم الحتمية حتى لو${\displaystyle P}$و${\displaystyle Q}$كلاهما حتمي: إذا${\displaystyle P}$و${\displaystyle Q}$كلاهما يستطيعان نقل نفس الحدث، إذن${\displaystyle P\;|||\;Q}$يختار بشكل غير حتمي أي من العمليتين نقلت ذلك الحدث. ^{[ 18 ]}

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

يمثل عامل التوازي في الواجهة (أو التوازي المعمم) نشاطًا متزامنًا يتطلب تزامنًا بين العمليات المكونة: لـ${\displaystyle P\;|[X]|\;Q}$أي حدث في مجموعة الواجهة${\displaystyle X\subseteq \Sigma }$لا يمكن أن يحدث ذلك إلا عندما يكون كلاهما${\displaystyle P}$و${\displaystyle Q}$قادرون على المشاركة في ذلك الحدث. ^{[ 18 ]}

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

إخفاء

يوفر عامل الإخفاء طريقة لتجريد العمليات عن طريق جعل بعض الأحداث غير قابلة للملاحظة من قبل البيئة.${\displaystyle P\setminus X}$هي العملية${\displaystyle P}$مع تحديد الحدث${\displaystyle X}$مختفي.

مثال بسيط على الاختباء هو${\displaystyle (a\to P)\setminus \{a\}}$وبافتراض أن الحدث${\displaystyle a}$لا يظهر في${\displaystyle P}$، ببساطة يختزل إلى${\displaystyle P}$تُستوعب الأحداث الخفية كأفعال تاو ، وهي غير مرئية للبيئة ولا يمكن التحكم بها. يُدخل وجود الإخفاء سلوكًا إضافيًا يُسمى التباعد ، حيث يتم تنفيذ سلسلة لا نهائية من أفعال تاو. ويتم التقاط هذا بواسطة العملية.${\displaystyle \mathbf {div} }$، الذي يقتصر سلوكه على أداء أفعال τ إلى الأبد. ^{[ 18 ]} على سبيل المثال،${\displaystyle (\mu Pa\to P)\setminus \{a\}}$يعادل${\displaystyle \mathbf {div} }$.

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

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

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

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

يمكن وضع هاتين العمليتين بالتوازي، بحيث تتفاعلان مع بعضهما البعض. ويعتمد سلوك العملية المركبة على الأحداث التي يجب أن تتزامن عليها العمليتان المكونتان لها. وبالتالي،

$${\displaystyle \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} }$$

أما إذا كانت المزامنة مطلوبة فقط على "العملة"، فسنحصل على

$${\displaystyle \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)}$$

إذا قمنا بتجريد هذه العملية المركبة الأخيرة عن طريق إخفاء أحداث "العملة" و"البطاقة"، أي

$${\displaystyle \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\}}$$

نحصل على العملية غير الحتمية

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

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

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

$${\displaystyle {\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}}}$$

لاحظ أنه، حرصًا على الإيجاز، فإن الصيغة المذكورة أعلاه تحذف الـ${\displaystyle \mathbf {div} }$العملية، التي تمثل التباعد ، بالإضافة إلى عوامل تشغيل مختلفة مثل التوازي الأبجدي، والتوصيل، والخيارات المفهرسة.

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

النماذج الدلالية الرئيسية الثلاثة لـ CSP هي نموذج الآثار ، ونموذج حالات الفشل المستقرة ، ونموذج حالات الفشل/الاختلافات . توفر عمليات الربط الدلالي من تعبيرات العمليات إلى كل نموذج من هذه النماذج الثلاثة الدلالات الدلالية لـ CSP. ^{[ 1 ]}

تسمح الدلالات التفسيرية بتعريفات متعددة لترتيب جزئي للتحسين على العمليات، والتي بدورها يمكن استخدامها لتمثيل العديد من خصائص العمليات بشكل أنيق. بشكل عام،${\displaystyle P\sqsubseteq Q}$يشير${\displaystyle Q}$يُحسّن${\displaystyle P}$.

لعلّ أشهر أدوات حل مشكلات إرضاء القيود (CSP) هي أداة تحسين حالات الفشل والاختلاف (FDR )، وهي منتج تجاري طوّرته في الأصل شركة Formal Systems (Europe) Ltd. غالبًا ما يُوصف FDR بأنه مدقق نماذج ، ولكنه في الواقع مدقق تحسين ، إذ يحوّل تعبيرين من تعبيرات عمليات CSP إلى أنظمة انتقال مُصنّفة (LTSs)، ثم يحدد ما إذا كانت إحدى العمليتين تحسينًا للأخرى ضمن نموذج دلالي مُحدد (آثار، أو حالات فشل، أو حالات فشل/اختلاف). ^{[ 20 ]} يطبّق FDR خوارزميات ضغط فضاء الحالة المختلفة على أنظمة الانتقال المُصنّفة للعملية لتقليل حجم فضاء الحالة الذي يجب استكشافه أثناء فحص التحسين. وقد أعقب FDR كلٌّ من FDR2 وFDR3 وFDR4. ^{[ 21 ]}

مدقق تحسين أديلايد ( ARC ) ^{[ 22 ]} هو مدقق لتحسين مسائل إرضاء القيود (CSP) طوّره فريق النمذجة والتحقق الرسمي في جامعة أديلايد . يختلف ARC عن FDR2 في أنه يُمثّل عمليات CSP داخليًا على شكل مخططات قرار ثنائية مُرتبة (OBDDs)، مما يُخفف من مشكلة تضخم الحالات في تمثيلات LTS الصريحة دون الحاجة إلى استخدام خوارزميات ضغط فضاء الحالة مثل تلك المستخدمة في FDR2.

مشروع ProB ^{[ 23 ]} ، الذي يستضيفه معهد المعلوماتية بجامعة هاينريش هاينه في دوسلدورف، أُنشئ في الأصل لدعم تحليل المواصفات المُنشأة باستخدام طريقة B. إلا أنه يدعم أيضًا تحليل عمليات CSP من خلال التحقق من التحسين والتحقق من نموذج LTL . ويمكن استخدام ProB أيضًا للتحقق من خصائص مواصفات CSP وB المُدمجة. وقد تم دمج مُحرك ProBE CSP في FDR3.

مجموعة أدوات تحليل العمليات (PAT) ^{[ 24 ] [ 25 ]} هي أداة لتحليل CSP طُوّرت في كلية علوم الحاسوب بالجامعة الوطنية في سنغافورة . تُتيح PAT إجراء عمليات التحقق من التحسين، والتحقق من نموذج LTL، ومحاكاة عمليات CSP وTimed CSP. تُوسّع لغة عمليات PAT نطاق CSP بدعم المتغيرات المشتركة القابلة للتغيير، وتمرير الرسائل غير المتزامن، ومجموعة متنوعة من بنيات العمليات المتعلقة بالإنصاف والكمية الزمنية . يقوم مبدأ التصميم الأساسي للغة عمليات PAT على دمج لغة مواصفات عالية المستوى مع البرامج الإجرائية (على سبيل deadlineالمثال waituntil، قد يكون الحدث في PAT برنامجًا تسلسليًا أو حتى استدعاء مكتبة C# خارجية) لزيادة القدرة على التعبير. تُوفّر المتغيرات المشتركة القابلة للتغيير والقنوات غير المتزامنة اختصارًا مناسبًا لأنماط نمذجة العمليات المعروفة المستخدمة في CSP القياسي. يُشابه بناء جملة PAT بناء جملة CSP _M ، ولكنه ليس مطابقًا له تمامًا . ^{[ 26 ]} الاختلافات الرئيسية بين بناء جملة PAT و CSP _M القياسي هي استخدام الفواصل المنقوطة لإنهاء تعبيرات العملية، وإدراج السكر النحوي للمتغيرات والتعيينات، واستخدام بناء جملة مختلف قليلاً للاختيار الداخلي والتركيب المتوازي.

يقوم VisualNets ^{[ 27 ]} بإنتاج تصورات متحركة لأنظمة CSP من المواصفات، ويدعم CSP الموقوت.

CSPsim ^{[ 28 ]} هو برنامج محاكاة كسول. لا يقوم بفحص نموذج CSP، ولكنه مفيد لاستكشاف الأنظمة الكبيرة جدًا (التي قد تكون لا نهائية).

SyncStitch ^{[ 29 ]} هو برنامج لفحص تحسينات CSP، مزود ببيئة تفاعلية للنمذجة والتحليل. يحتوي على محرر رسومي لمخطط انتقال الحالة. يمكن للمستخدم نمذجة سلوك العمليات ليس فقط باستخدام تعبيرات CSP، بل أيضًا باستخدام مخططات انتقال الحالة. تُعرض نتائج الفحص أيضًا بشكل رسومي على هيئة أشجار حسابية، ويمكن تحليلها تفاعليًا باستخدام أدوات فحص إضافية. بالإضافة إلى فحوصات التحسين، يمكنه إجراء فحوصات حالات الجمود وحالات التعطل.