Перегляд вихідного коду сторінки Комунікуючі послідовні процеси

'''Взаємодія послідовних процесів''' ({{lang-en|Communicating Sequential Processes, CSP}}) — [[формальна мова]] для опису закономірностей взаємодії в [[Рівночасність (інформатика)|рівночасних системах]].<ref name="roscoe">{{cite book|first=A. W.|last=Roscoe|authorlink=Bill Roscoe|title=The Theory and Practice of Concurrency|publisher=[[Prentice Hall]]|isbn=0-13-674409-5|year=1997|url-access=registration|url=https://archive.org/details/theorypracticeof00rosc}}</ref> Це член сім'ї математичних теорій рівночасності, відомої як алгебра або {{нп|числення процесів||en|Process calculus}}, в основі якої лежить [[обмін повідомленнями]] через [[канал (програмування)|канали]]. CSP відіграв важливу роль у розробці мови програмування [[occam]]<ref name="roscoe"/><ref>{{cite book|last=INMOS|authorlink=INMOS|url=http://www.wotug.org/occam/documentation/oc21refman.pdf|format=PDF|title=occam 2.1 Reference Manual|publisher=SGS-THOMSON Microelectronics Ltd.|date=1995-05-12|accessdate=27 Вересня 2017|archive-date=1 Серпня 2020|archive-url=https://web.archive.org/web/20200801234838/http://www.wotug.org/occam/documentation/oc21refman.pdf}}, INMOS document 72 occ 45 03</ref>, а також вплинув на дизайн таких мов програмування, як [[Limbo (мова програмування)|Limbo]]<ref>{{cite web|title=Resources about threaded programming in the Bell Labs CSP style|url=http://swtch.com/~rsc/thread/|accessdate=2010-04-15|archive-date=26 Квітня 2013|archive-url=https://web.archive.org/web/20130426081645/http://swtch.com/~rsc/thread/}}</ref>, {{iw|RaftLib}}, [[Go (мова програмування)|Go]]<ref name="golang">{{cite web |title=Language Design FAQ: Why build concurrency on the ideas of CSP? |url=http://golang.org/doc/go_faq.html#csp |accessdate=27 Вересня 2017 |archive-date=2 Січня 2013 |archive-url=https://web.archive.org/web/20130102205822/http://golang.org/doc/go_faq.html#csp }}</ref>, та бібліотеки core.async в [[Clojure]]<ref>{{Cite book
|title = Clojure for the Brave and True
|last = Higginbotham
|first = Daniel
|chapter = Mastering Concurrent Processes with core.async
|url = https://www.braveclojure.com/core-async/
|edition = 1 edition
|publisher = No Starch Press
|location = San Francisco
|isbn = 978-1-59327-591-4
|accessdate = 27 Вересня 2017
|archive-date = 28 Вересня 2017
|archive-url = https://web.archive.org/web/20170928005536/https://www.braveclojure.com/core-async/
}}</ref>.

CSP описує послідовні процеси, які взаємодіють лише через передачу повідомлень (і не через використання [[Спільна пам’ять|спільної пам'яті]]).<ref>{{Cite AV media| people = Coding Tech| title = Concurrency Patterns In Go| accessdate = 2018-08-09| url = https://www.youtube.com/watch?v=YEKjSzIwAdA}} {{Cite web |url=https://www.youtube.com/watch?v=YEKjSzIwAdA |title=Архівована копія |accessdate=2018-08-09 |archive-date=2018-12-30 |archive-url=https://web.archive.org/web/20181230081619/https://www.youtube.com/watch?v=YEKjSzIwAdA }}</ref>

CSP був вперше описаний в 1978, у публікації [[Тоні Гоар|Гоара]]<ref name="hoare1978">{{cite journal|last=Hoare
|first=C. A. R.
|authorlink=C. A. R. Hoare
|title=Communicating sequential processes
|journal=[[Communications of the ACM]]
|volume=21
|issue=8
|pages=666–677
|year=1978
|doi=10.1145/359576.359585}}
</ref>, але з тих пір суттєво змінився<ref name="25years">{{cite book
|last=Abdallah | first = Ali E.| last2 = Jones | first2 = Cliff B. | last3 = Sanders | first3 = Jeff W.
|title=Communicating Sequential Processes: The First 25 Years
|series=[[LNCS]]
|volume=3525
|publisher=Springer
|year=2005
|url=https://www.springer.com/computer/theoretical+computer+science/foundations+of+computations/book/978-3-540-25813-1}}
</ref>. CSP практично застосовувався в промисловості як інструмент для [[Формальна специфікація|специфікації і верифікації]] рівночасних аспектів різних систем, таких як [[Transputer]] T9000<ref name="barrett">
{{cite journal|last=Barrett
|first=G.
|title=Model checking in practice: The T9000 Virtual Channel Processor
|journal=[[IEEE]] Transactions on Software Engineering
|volume=21
|issue=2
|pages=69–78
|year=1995
|doi=10.1109/32.345823}}</ref>, а також безпечної системи електронної комерції.<ref name="hall">{{cite journal
 |last         = Hall
 |first        = A
 |first2       = R.
 |last2        = Chapman
 |url          = http://www.anthonyhall.org/c_by_c_secure_system.pdf
 |format       = PDF
 |title        = Correctness by construction: Developing a commercial secure system
 |journal      = [[IEEE]] Software
 |volume       = 19
 |issue        = 1
 |pages        = 18–25
 |year         = 2002
 |doi          = 10.1109/52.976937
 |accessdate   = 27 Вересня 2017
 |archive-date = 2 Грудня 2020
 |archive-url  = https://web.archive.org/web/20201202131145/http://www.anthonyhall.org/c_by_c_secure_system.pdf
}}</ref> Теорія самого CSP досі є предметом активних досліджень, у тому числі робота з підвищення його спектру практичної застосовності (наприклад, збільшення масштабів систем, які можуть бути проаналізовані).<ref>
{{Cite journal| last = Creese | first = S.|title=Data Independent Induction: CSP Model Checking of Arbitrary Sized Networks|version=D. Phil.|publisher=[[Oxford University]]|year=2001}}
</ref>

== Історія ==
Версія CSP, представлена в оригінальній публікації Хоара 1978 року була, по суті, рівночасною мовою програмування, а не {{iw|числення процесів|численням процесів|en|process calculus}}. CSP мав принципово інший синтаксис, ніж у більш пізніх версіях, не володів математично-визначеною семантикою<ref name="hoare">{{cite book|last=Hoare|first=C. A. R.|authorlink=C. A. R. Hoare|title=Communicating Sequential Processes|publisher=Prentice Hall|isbn=0-13-153289-8|year=1985}}</ref> і не був в змозі представляти {{iw|необмежений недетермінізм|||unbounded nondeterminism}}.<ref name="clinger1981">{{Cite journal|first=William|last=Clinger|authorlink=Вільям Клінґер (вчений)|title=Foundations of Actor Semantics|url=https://dspace.mit.edu/handle/1721.1/6935|publisher=MIT|version=Mathematics Doctoral Dissertation|date=June 1981|journal=|accessdate=8 Лютого 2018|archive-date=25 Липня 2019|archive-url=https://web.archive.org/web/20190725182014/https://dspace.mit.edu/handle/1721.1/6935}}</ref> Програми в оригінальному CSP були написані, як паралельні композиції фіксованого числа послідовних процесів, які спілкувалися один з одним строго через синхронну передачу повідомлень. На відміну від пізніших версій CSP, кожному процесу призначалось явне ім'я, а джерело або адресат повідомлення визначались задаванням імені передбачуваного відправника або процесу отримувача. Наприклад процес

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

без перестану отримує символ від процесу <code>west</code> та відправляє цей символ процесу <code>east</code>. Паралельна композиція

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

присвоює ім’я <code>west</code> процесу <code>DISASSEMBLE</code>, <code>X</code> процесу <code>COPY</code> і <code>east</code> процесу <code>ASSEMBLE</code> та виконує ці три процеси паралельно.<ref name="hoare1978" />

Після публікації оригінальної версії CSP, Хоар, Стівен Брукс та [[Біл Роско]] розвинули та вдосконалили теорію CSP до її сучасної форми, алгебри процесів. Підхід використаний при перетворенні CSP в алгебру процесів, був обраний під впливом роботи [[Робін Мілнер|Робіна Мілнера]] над {{iw|Числення комунікуючих систем|Численням комунікуючих систем||Calculus of Communicating Systems}} (CCS) та навпаки, CSP вплинула на CCS. Теоретична версія CSP була спочатку представлена у статті Брукса, Хоара і Роско 1984р,<ref>{{cite journal|first=Stephen|last=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 = A Theory of Communicating Sequential Processes|journal=[[Journal of the ACM]]|volume=31|issue=3|pages=560–599|year=1984|doi=10.1145/828.833}}</ref> пізніше – у книзі Хоара «Communicating Sequential Processes»<ref name="hoare" />, що була опублікована у 1985р. У вересні 2006 ця книга все ще була однією з найбільш цитованих публікацій у комп’ютерних науках всіх часів за версією [[Citeseer]]. Теорія CSP пережила декілька незначних змін з моменту публікації книги Хоара. Більшість змін була викликана появою автоматизованих інструментів для аналізу та верифікації процесів. «The Theory and Practice of Concurrency» від Роско описує новішу версію CSP<ref name="roscoe" />.

=== Використання ===
Раннім і важливим використанням CSP була специфікація і верифікація елементів [[транспютер]]а INMOS T9000, комплексного суперскалярного конвеєрного процесора, розробленого для підтримки крупномасштабного мультипроцесингу. CSP було використано у верифікації коректності конвеєра та процесора віртуального каналу ({{lang-en|Virtual Channel Processor}}), що керував позачіповими комунікаціями процесора.<ref name="barrett" />

Індустріальне використання CSP у розробці програмного забезпечення, зазвичай, сфокусоване на надійних та критично-безпечних системах. Наприклад, Bremen Institute for Safe Systems та [[DaimlerChrysler Aerospace|Daimler-Benz Aerospace]] змоделювали з допомогою CSP систему керування помилками та інтерфейс [[авіоніка|авіоніки]] (з приблизно 23000 рядків коду) для використання на Міжнародній космічній станції, та проаналізували модель, перевіривши відсутність в їхньому проекті [[Взаємне блокування|взаємних блокувань]] та [[livelock]]-ів..<ref>{{cite conference|first=B. |last=Buth|author2=M. Kouvaras |author3=J. Peleska |author4=H. Shi |title=Deadlock analysis for a fault-tolerant system|booktitle=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=Combining methods for the livelock analysis of a fault-tolerant system|booktitle=Proceedings of the 7th International Conference on Algebraic Methodology and Software Technology (AMAST’98)|pages=124–139|date=January 1999}}</ref> Процес моделювання та аналізу допоміг відшукати помилки, які було б важко знайти, використовуючи лише тестування. Аналогічно, {{iw|Praxis High Integrity Systems}} використали CSP-моделювання і аналіз під час розробки програмного забезпечення (приблизно 100000 рядків коду) для безпечної сертифікації смарт-карток. Praxis стверджує, що система має значно меншу частоту дефектів, порівняно з аналогічними системами.<ref name="hall" />

Оскільки CSP є вдалим рішенням у моделюванні та аналізі систем, які містять складний обмін повідомленнями, він також використовується у перевірці безпеки протоколів зв'язку. Гарним прикладом такого застосування є використання CSP та {{iw|FDR2|FDR}} для знаходження невідомої раніше атаки на [[протокол Нідгема — Шредера|протокол аутентифікації з відкритим ключем Нідгема — Шредера]], а потім розробити виправлену версію протоколу, що спроможна протистояти атаці.<ref>{{cite web|first=G. |last=Lowe|title=Breaking and fixing the Needham-Schroeder public-key protocol using FDR|url=https://www.cs.utexas.edu/~shmat/courses/cs6431/lowe.pdf}}</ref>

== Неформальний опис ==
Виходячи з назви, CSP дозволяє опис систем з точки зору складових процесів, що працюють незалежно та взаємодіють один з одним виключно через [[обмін повідомленнями]]. Тим не менш, слово "послідовні" в назві комунікуючих послідовних процесів на сьогодні дещо недоречне, тому що сучасна CSP дозволяє визначати процеси компоненти як послідовними процесами, так і паралельною композицією більш примітивних процесів. Зв’язки між різними процесами і спосіб взаємодії процесу зі своїм середовищем описуються за допомогою різних операторів {{iw|числення процесів|алгебри процесів||process calculi}}. Використовуючи такий алгебраїчний підхід, доволі складний опис процесу може бути легко побудований з декількох примітивних елементів.

=== Примітиви ===
CSP забезпечує два класи примітивів в алгебрі процесів:
; Події
: Події являють собою комунікацію чи інші взаємодії. Припускається що вони нероздільні і миттєві. Вони можуть мати як атомарні імена (наприклад ''вкл'', ''викл''), складені імена (наприклад ''кран.відкрити'', ''кран.закрити''), або події вводу/виводу (наприклад ''mouse?xy'', ''screen!bitmap'').
; Примітивні процеси.
: Примітивні процеси задають фундаментальні поведінки, наприклад ''STOP'' (процес який не комунікує, який також називають [[deadlock]]), та ''SKIP'' (який завжди має успішне завершення).

=== Алгебраїчні оператори ===
CSP має широкий спектр алгебраїчних операторів. Основними з них є:

;Префікс
:Оператор «префікс» з'єднує подію і процес для отримання нового процесу. Наприклад:

::<math>a \rightarrow P</math>

:процес який передає в навколишнє середовище подію <math>\mathit{a}</math>, після чого поводиться як процес <math>\mathit{P}</math>.

;Детермінований вибір
:Оператор детермінованого (або зовнішнього) вибору дозволяє визначити майбутній розвиток процесу як вибір між двома складовими процесами і дозволяє навколишньому середовищу зробити вибір по початковій події одного з процесів. Наприклад:

::<math>\left(a \rightarrow P\right) \Box \left(b \rightarrow Q\right)</math>

:це процес, який залежно від початкової події, <math>\mathit{a}</math> або <math>\mathit{b}</math>, поводить себе як <math>\mathit{P}</math> або <math>\mathit{Q}</math>. Якщо одночасно відбудуться і <math>\mathit{a}</math> і <math>\mathit{b}</math>, вибір буде здійснено недетерміновано.

;Недетермінований вибір
:Оператор недетермінованого (або внутрішнього) вибору дозволяє визначити майбутній розвиток процесу як вибір між двома складовими процесами, але не надає навколишньому середовищу контроль над цим вибором. Наприклад:

::<math>\left(a \rightarrow P\right) \sqcap \left(b \rightarrow Q\right)</math>

:може поводити себе, як <math>\left(a \rightarrow P\right)</math> чи <math>\left(b \rightarrow Q\right)</math>. Він може відкинути <math>\mathit{a}</math> або <math>\mathit{b}</math> і зобов’язаний продовжити роботу, якщо середовище пропонує і <math>\mathit{a}</math>, і <math>\mathit{b}</math>. Недетермінізм може бути ненавмисно введений у детермінований вибір, якщо початкові події обох сторін є ідентичними. Наприклад:

::<math>\left(a \rightarrow a \rightarrow STOP\right) \Box \left(a \rightarrow b \rightarrow STOP\right)</math>

:еквівалентно до

::<math>a \rightarrow \left(\left(a \rightarrow STOP\right) \sqcap \left(b \rightarrow STOP\right)\right)</math>


;Чергування
:Оператор чергування представляє абсолютно незалежну одночасну діяльність.

::<math>P \;\vert\vert\vert\; Q</math>

:поводить себе одночасно і як <math>\mathit{P}</math>, і як <math>\mathit{Q}</math>. Події з обох процесів довільно чергуються у часі.

;Інтерфейсний паралелелізм
:Оператор інтерфейсного паралелелізму представляє одночасну діяльність, що потребує синхронізації між складовими процесами: будь-яка подія з набору інтерфейсів може відбутися лише тоді, коли всі складові процеси мають можливість виконати цю подію. Наприклад:

::<math>P \left\vert\left[ \left\{ a \right\} \right]\right\vert Q</math>

:перед виконанням події <math>\mathit{a}</math> необхідно, щоб і <math>\mathit{P}</math>, і <math>\mathit{Q}</math> були в змозі виконати цю подію. Тому, наприклад, процес

::<math>\left(a \rightarrow P\right) \left\vert\left[ \left\{ a \right\} \right]\right\vert \left(a \rightarrow Q\right)</math>

:може виконати подію <math>\mathit{a}</math> і стати процесом

::<math>P \left\vert\left[ \left\{ a \right\} \right]\right\vert Q</math>

:в той час як на

::<math>\left (a \rightarrow P\right ) \left\vert\left[ \left\{ a, b \right\} \right]\right\vert \left(b \rightarrow Q\right)</math>

:чекає deadlock.

;Приховування
:Оператор приховування дозволяє робити деякі події неможливими для спостереження. Тривіальний приклад:

::<math>\left(a \rightarrow P\right) \setminus \left\{ a \right\}</math>

:який, припустивши, що подія <math>\mathit{a}</math> не з’являється у <math>\mathit{P}</math>, спрощується до

::<math>\mathit{P}</math>

=== Рекурсія ===
Префіксний запис дозволяє нам описувати поведінку скінченного процесу, але у випадку торгового автомата буде не зручно описувати все його життя з його сотнями і тисячами продажів. Таким чином нам потрібен спосіб для опису повторюваних дій, що дасть нам побічно можливість описувати нескінченно живуть процеси.

Розглянемо механічний годинник, зважаючи на те, що нас цікавлять лише його тіки, тоді:

''αCLOCK = {tick}''

Після того як годинник тікнув, він залишаться тим же годинником, тоді ми можемо сказати, що об'єкт після тіку стає годинником що виглядає наступним чином:

''CLOCK = (tick → CLOCK)''

Підставляючи CLOCK в праву частину ми будемо отримувати:

CLOCK

    = (Tick → CLOCK) [початкове рівняння]

    = (Tick → (tick → CLOCK)) [перша підстановка]

    = (Tick → (tick → (tick → CLOCK))) [друга підстановка]

Отже поведінку годинника може бути описано як нескінченна кількість повторюючихся тиків:

''tick → tick → tick → · · ·''

Даний спосіб посилання на себе буде працювати тільки у випадку якщо з правого боку рівняння вказано вираз, що починається з префіксу, наприклад рівняння:

''X = X''

Нічого не визначає, тому йому відповідає будь-який процес. Будемо далі називати опис процесу починаються з префіксу «захищеним». Таким чином якщо ''F (X'') захищене вираз містить ім'я процесу ''X'' і ''αX = A'', то рівняння:

''X = F (X)''

має єдине рішення з алфавітом ''A.''

Твердження про те, що захищений вираз має рішення і воно, можливо, унікальне легко демонструється за допомогою методу підстановок: підставляючи у вираз процес ми його подовжуємо, що може тривати необмежено, таким чином ми можемо написати довільно довгий (але кінцевий) опис процесу, а якщо два процеси протягом довільно довгого часу мають однакову поведінку, то ми говоримо що вони однакові.

== Формальне визначення ==

=== Синтаксис ===
Синтаксис CSP визначає «легальні» способи комбінування подій і процесів. Нехай <math>\mathit{e}</math> - подія, <math>\mathit{X}</math> - множина подій. Тоді базовий синтаксис CSP можна визначити як:

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

Відзначимо, що в інтересах стислості, описаний синтаксис опускає процес <math>\mathbf{div}</math>, який являє собою «{{iw|розбіжний процес|||Divergence (computer science)}}», а також різні оператори, такі як алфавітний паралелелізм, конвеєризація та індексований вибір.

=== Формальна семантика ===

CSP був доповнений кількома різними [[Семантика#В програмуванні|семантиками]], які визначають значення синтаксично правильного виразу CSP. Теорія комунікуючих послідовних процесів включає взаємно узгоджені [[денотативна семантика|денотативну семантику]], [[алгебраїчна семантика|алгебраїчну семантику]] та [[операційна семантика|операційну семантику]]. 

==== Денотативна семантика ====
Основними денотативними моделями в CSP є ''модель слідів'' ({{lang-en|traces model}}), модель ''стабільних невдач'' ({{lang-en|stable failures}}), та модель ''невдач/розбіжностей'' ({{lang-en|failures/divergences}}). Відображення з виразів що задають процеси на кожну з цих трьох моделей і задають денотативну смантику CSP.<ref name="roscoe" />

''Модель слідів'' визначає значення виразу процесу як множину послідовностей подій (слідів) які можна спостерігати при роботі процесу. Наприклад:

:* <math>\mathit{traces}\left(\mathit{STOP}\right) = \left\{ \langle\rangle \right\}</math> тому що <math>\mathit{STOP}</math> не генерує ніяких подій
:* <math>\mathit{traces}\left(a\rightarrow b \rightarrow \mathit{STOP}\right) = \left\{\langle\rangle ,\langle a \rangle, \langle a, b \rangle \right\}</math> тому що процес <math>(a\rightarrow b \rightarrow \mathit{STOP})</math> може не згенерувати події, згенерувати подію <math>a</math>, або послідовність подій <math>a, b</math>

Більш формально, процес <math>P</math> в моделі процесів описується як <math>\mathit{traces}\left(P\right) \subseteq \Sigma^{\ast}</math> такий що:
# <math>\langle\rangle \in \mathit{traces}\left(P\right)</math> (тобто <math>\mathit{traces}\left(P\right)</math> містить порожню послідовність)
# <math>s_1 \smallfrown s_2 \in \mathit{traces}\left(P\right) \implies s_1 \in \mathit{traces}\left(P\right)</math> (тобто <math>\mathit{traces}\left(P\right)</math> замкнута операцією взяття префіксу)
де <math>\Sigma^{\ast}</math> множина всіх можливих скінченних послідовностей подій.

''Модель стабільних невдач'' розширює модель слідів множинами відмов, які є множинами подій <math>X \subseteq \Sigma</math> які процес може відмовитись виконати. ''Невдача'' це пара <math>\left(s,X\right)</math>, що складається зі сліду <math>s</math>, та множини невдач <math>X</math> яка визначає події які процес може відмовитись виконати коли він виконав слід <math>s</math>. Спостережувана поведінка процесу в моделі стабільних невдач описується парою <math>\left(\mathit{traces}\left(P\right), \mathit{failures}\left(P\right)\right)</math>. Наприклад,

:* <math>\mathit{failures}\left(\left(a \rightarrow \mathit{STOP}\right) \Box \left(b \rightarrow \mathit{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>\mathit{failures}\left(\left(a \rightarrow \mathit{STOP}\right) \sqcap \left(b \rightarrow \mathit{STOP}\right)\right) = \left\{ \left(\langle\rangle,\left\{a\right\}\right), \left(\langle\rangle,\left\{b\right\}\right), \left(\langle a \rangle, \emptyset\right), \left(\langle b \rangle, \emptyset\right),
\left(\langle a \rangle, \left\{a,b\right\}\right), \left(\langle b \rangle,\left\{a,b\right\}\right) \right\}</math>

''Модель невдач/розбіжностей'' ще більше розвиває модель невдач, аби працювати з [[розбіжність (комп'ютерні науки)|розбіжністю]]. Семантикою процесу в моделі невдач/розбіжностей є пара <math>\left(\mathit{failures}_\perp\left(P\right), \mathit{divergences}\left(P\right)\right)</math> де <math>\mathit{divergences}\left(P\right)</math> визначається як множина всіх слідів які можуть привести до розбіжної поведінки, а <math>\mathit{failures}_\perp\left(P\right) = \mathit{failures}\left(P\right) \cup \left\{\left(s,X\right) \mid s \in \mathit{divergences}\left(P\right)\right\}</math>.

== Пов’язані засоби специфікації та формалізми ==
Деякі інші мови специфікації та формалізми були виведені з класичного CSP, включаючи:
* Timed CSP, який об’єднує в собі часову інформацію про системи реального часу
* Receptive Process Theory, спеціалізація CSP, що передбачає асинхронні операції відправлення
* CSPP
* HSCSP
* Wright, мова опису архітектури
* TCOZ, інтеграція Timed CSP і Object Z
* Circus, інтеграція CSP і Z
* CML (Compass Modelling Language), комбінація Circus і VDM, створена для моделювання SoS (Systems of Systems)
* CspCASL, розширення CCCASL, що інтегрує CSP
* LOTOS, міжнародний стандарт, що містить в собі особливості CSP і CCS

== Зноски ==
<references />

== Посилання ==
* https://swtch.com/~rsc/thread/squint.pdf {{Webarchive|url=https://web.archive.org/web/20180111164944/https://swtch.com/~rsc/thread/squint.pdf |date=11 Січня 2018 }}

[[Категорія:Мови специфікацій]]
[[Категорія:Конкурентні обчислення]]