Коммуникация последовательных процессов

Не путать с проблемой удовлетворения ограничений .

В информатике коммуникативные последовательные процессы ( CSP ) являются формальным языком для описания моделей взаимодействия в параллельных системах . Это член семейства математических теорий параллелизма, известных как алгебры процессов или исчисления процессов , основанные на передаче сообщений по каналам . CSP оказал большое влияние на разработку occam. языка программирования а также повлиял на дизайн таких языков программирования, как Limbo , РафтЛиб , Эрланг , Идти , Crystal и Clojure . core.async

CSP был впервые описан в статье Тони Хоара в 1978 году . но с тех пор существенно изменился. CSP практически применяется в промышленности как инструмент для определения и проверки параллельных аспектов множества различных систем, таких как T9000 Transputer , а также безопасная система электронной коммерции . Сама теория CSP также до сих пор является предметом активных исследований, включая работы по расширению ее практической применимости (например, увеличение масштаба систем, которые можно легко проанализировать).

История

Версия CSP, представленная в оригинальной статье Хоара 1978 года, по существу представляла собой язык параллельного программирования, а не исчисление процессов . Он имел существенно другой синтаксис, чем более поздние версии CSP, не обладал математически определенной семантикой. и не смог представить неограниченный недетерминизм . Программы в оригинальном CSP были написаны как параллельная композиция фиксированного числа последовательных процессов, взаимодействующих друг с другом строго посредством синхронной передачи сообщений. В отличие от более поздних версий CSP, каждому процессу присваивалось явное имя, а источник или место назначения сообщения определялись путем указания имени предполагаемого процесса отправки или получения. Например, процесс

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

неоднократно получает символ от процесса с именем west и отправляет этот символ в процесс с именем east. Параллельная композиция

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

присваивает имена west к DISASSEMBLE процесс, X к COPY процесс, и east к ASSEMBLE процесс и выполняет эти три процесса одновременно.

После публикации оригинальной версии CSP Хоар, Стивен Брукс и А. В. Роско разработали и усовершенствовали теорию CSP до ее современной алгебраической формы. На подход, использованный при разработке CSP в алгебру процессов, повлияла Робина Милнера работа по исчислению коммуникационных систем (CCS) и наоборот. Теоретическая версия CSP была первоначально представлена ​​в 1984 году в статье Брукса, Хоара и Роско: и позже в книге Хоара «Связь последовательных процессов» : который был опубликован в 1985 году. В сентябре 2006 года эта книга по-прежнему оставалась третьим по цитируемости справочником по информатике всех времен по данным Citeseer. (хотя и ненадежный источник из-за характера отбора проб). Теория CSP претерпела несколько незначительных изменений со времени публикации книги Хоара. Большинство этих изменений было вызвано появлением автоматизированных инструментов для анализа и проверки процессов CSP. Роско «Теория и практика параллелизма». описывает эту новую версию CSP.

Приложения

Ранним и важным применением CSP было его использование для спецификации и проверки элементов INMOS T9000 Transputer , сложного суперскалярного конвейерного процессора, предназначенного для поддержки крупномасштабной многопроцессорной обработки. CSP использовался для проверки правильности как конвейера процессора, так и процессора виртуального канала, который управлял внешней связью процессора.

Промышленное применение CSP для разработки программного обеспечения обычно фокусируется на надежных и критически важных для безопасности системах. Например, Бременский институт безопасных систем и компания Daimler-Benz Aerospace смоделировали в CSP систему управления отказами и интерфейс авионики (состоящий из около 23 000 строк кода), предназначенных для использования на Международной космической станции, и проанализировали модель, чтобы подтвердить, что в их конструкции не было тупиковых и живых блокировок. Процесс моделирования и анализа позволил выявить ряд ошибок, которые было бы трудно обнаружить с помощью одного лишь тестирования. Аналогичным образом компания Praxis High Integrity Systems применила моделирование и анализ CSP во время разработки программного обеспечения (около 100 000 строк кода) для безопасного центра сертификации смарт-карт, чтобы убедиться, что их конструкция безопасна и не имеет тупиковых ситуаций. Praxis утверждает, что в этой системе гораздо меньший процент дефектов, чем в сопоставимых системах.

Поскольку CSP хорошо подходит для моделирования и анализа систем, включающих сложный обмен сообщениями, он также применяется для проверки протоколов связи и безопасности. Ярким примером такого рода приложений является использование Лоу CSP и средства проверки уточнений FDR для обнаружения ранее неизвестной атаки на протокол аутентификации с открытым ключом Нидхэма-Шредера , а затем для разработки исправленного протокола, способного отразить эту атаку.

Неофициальное описание

Как следует из названия, CSP позволяет описывать системы с точки зрения составных процессов, которые работают независимо и взаимодействуют друг с другом исключительно посредством передачи сообщений . Однако «последовательная» часть имени CSP теперь является неправильным употреблением, поскольку современный CSP позволяет определять процессы-компоненты как как последовательные процессы, так и как параллельную композицию более примитивных процессов. Отношения между различными процессами и способ взаимодействия каждого процесса со своей средой описываются с помощью различных алгебраических операторов процесса. Используя этот алгебраический подход, можно легко построить довольно сложные описания процессов из нескольких примитивных элементов.

Примитивы

CSP предоставляет два класса примитивов в своей алгебре процессов:

События

События представляют собой коммуникации или взаимодействия. Они считаются неделимыми и мгновенными. Это могут быть атомарные имена (например, on , off ), составные имена (например, Valve.open , Valve.close ) или события ввода/вывода (например, mouse?xy , screen!bitmap ).

Примитивные процессы

Примитивные процессы представляют фундаментальное поведение: примеры включают STOP (процесс, который ничего не передает, также называемый взаимоблокировкой ) и SKIP (который означает успешное завершение).

Алгебраические операторы

CSP имеет широкий набор алгебраических операторов. Основными из них являются:

Префикс

Префиксный оператор объединяет событие и процесс для создания нового процесса. Например,

$$a\to P$$

который желает взаимодействовать a со своей средой и после a ведет себя как процесс P. — это процесс ,

Детерминированный выбор

Оператор детерминированного (или внешнего) выбора позволяет определить будущую эволюцию процесса как выбор между двумя компонентными процессами и позволяет среде разрешить этот выбор, сообщив начальное событие для одного из процессов. Например,

$$(a\to P)\Box (b\to Q)$$

— это процесс, который готов сообщить начальные события a и b и впоследствии ведет себя как P или Q , в зависимости от того, какое начальное событие выбирает среда. Если бы и a, и b были сообщены одновременно, выбор был бы решен недетерминированно.

Недетерминированный выбор

Оператор недетерминированного (или внутреннего) выбора позволяет определить будущую эволюцию процесса как выбор между двумя составляющими процессами, но не позволяет среде контролировать, какой из составных процессов будет выбран. Например,

$$(a\to P)\sqcap (b\to Q)$$

может вести себя как $(a\to P)$ или $(b\to Q)$. Он может отказаться принять a или b и обязан сообщать только в том случае, если среда предлагает и a, и b . Недетерминизм может быть непреднамеренно привнесен в номинально детерминированный выбор, если исходные события обеих сторон выбора идентичны. Так, например,

$$(a\to a\to {\text{STOP}})\Box (a\to b\to {\text{STOP}})$$

эквивалентно

$$a\to {\big (}(a\to {\text{STOP}})\sqcap (b\to {\text{STOP}}){\big )}$$

Чередование

Оператор чередования представляет собой полностью независимую параллельную деятельность. Процесс

$$P\;|||\;Q$$

ведет себя как P и Q одновременно. События обоих процессов произвольно чередуются во времени.

Параллельный интерфейс

Оператор параллельного интерфейса представляет собой параллельную деятельность, требующую синхронизации между процессами компонентов: любое событие в наборе интерфейсов может произойти только тогда, когда все процессы компонентов могут участвовать в этом событии. Например, процесс

$$P\;|[\{a\}]|\;Q$$

требует, чтобы P и Q были в состоянии выполнить событие a, прежде чем это событие может произойти. Так, например, процесс

$$(a\to P)\;|[\{a\}]|\;(a\to Q)$$

может участвовать в событии а и стать процессом

$$P\;|[\{a\}]|\;Q$$

пока

$$(a\to P)\;|[\{a,b\}]|\;(b\to Q)$$

просто зайдет в тупик.

Скрытие

Оператор скрытия позволяет абстрагировать процессы, делая некоторые события ненаблюдаемыми. Тривиальный пример сокрытия:

$$(a\to P)\setminus \{a\}$$

что, предполагая, что событие a не появляется в P , просто сводится к

$$P$$

Примеры

Одним из типичных примеров CSP является абстрактное представление автомата по продаже шоколада и его взаимодействия с человеком, желающим купить шоколад. Этот торговый автомат может выполнять два разных события: «монета» и «шоколад», которые представляют собой внесение платежа и доставку шоколада соответственно. Автомат, который требует оплаты (только наличными) перед тем, как предложить шоколад, можно записать так:

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

Человека, который может решить использовать монету или карту для совершения платежей, можно смоделировать следующим образом:

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

Эти два процесса можно поставить параллельно, чтобы они могли взаимодействовать друг с другом. Поведение составного процесса зависит от событий, по которым два компонента процесса должны синхронизироваться. Таким образом,

$$\mathrm {VendingMachine} \left\vert \left[\left\{\mathrm {coin} ,\mathrm {card} \right\}\right]\right\vert \mathrm {Person} \equiv \mathrm {coin} \rightarrow \mathrm {choc} \rightarrow \mathrm {STOP}$$

тогда как если бы синхронизация требовалась только для «монеты», мы бы получили

$$\mathrm {VendingMachine} \left\vert \left[\left\{\mathrm {coin} \right\}\right]\right\vert \mathrm {Person} \equiv \left(\mathrm {coin} \rightarrow \mathrm {choc} \rightarrow \mathrm {STOP} \right)\Box \left(\mathrm {card} \rightarrow \mathrm {STOP} \right)$$

Если мы абстрагируем этот последний составной процесс, скрывая события «монеты» и «карты», т.е.

$$\left(\left(\mathrm {coin} \rightarrow \mathrm {choc} \rightarrow \mathrm {STOP} \right)\Box \left(\mathrm {card} \rightarrow \mathrm {STOP} \right)\right)\setminus \left\{\mathrm {coin,card} \right\}$$

мы получаем недетерминированный процесс

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

Это процесс, который либо предлагает событие «choc», а затем останавливается, либо просто останавливается. Другими словами, если мы будем рассматривать абстракцию как внешний взгляд на систему (например, тот, кто не видит решения, принятого этим человеком), недетерминизм будет введен .

Формальное определение

Синтаксис

Синтаксис 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}}$$

Обратите внимание, что в целях краткости в представленном выше синтаксисе опущена $\mathbf {div}$ процесс, который представляет расхождение , а также различные операторы, такие как параллель в алфавитном порядке, конвейеризация и индексированный выбор.

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

CSP наполнен несколькими различными формальными семантиками , которые определяют значение синтаксически правильных выражений CSP. Теория CSP включает взаимно согласованную денотационную семантику , алгебраическую семантику и операционную семантику .

Денотационная семантика

Тремя основными моделями CSP являются модель трасс , модель устойчивых сбоев и модель сбоев/расхождений . Семантические отображения выражений процесса в каждую из этих трех моделей обеспечивают денотационную семантику для 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} )$ можно наблюдать, что не было выполнено ни одного события, событие a или последовательность событий a, за которыми следует b.

Более формально смысл процесса P в модели следов определяется как $\mathrm {traces} \left(P\right)\subseteq \Sigma ^{\ast }$ такой, что:

1. $\langle \rangle \in \mathrm {traces} \left(P\right)$ (т.е. $\mathrm {traces} \left(P\right)$ содержит пустую последовательность)
2. $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\subseteq \Sigma$ что процесс может отказаться выполняться. Неудача – это пара $\left(s,X\right)$, состоящий из трассировки s и набора отказов X , который идентифицирует события, от которых процесс может отказаться после выполнения трассировки s . Наблюдаемое поведение процесса в модели устойчивых отказов описывается парой $\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. Ранние реализации инструментов использовали различные машиночитаемые синтаксисы для CSP, что делало входные файлы, написанные для разных инструментов, несовместимыми. Однако большинство инструментов CSP в настоящее время стандартизированы на машиночитаемом диалекте CSP, разработанном Брайаном Скаттергудом, иногда называемом _M. CSP Диалект CSP _M обладает формально определенной операционной семантикой , которая включает встроенный функциональный язык программирования .

Самым известным инструментом CSP, вероятно, является Failers/Divergence Refinement 2 FDR2 ( ), коммерческий продукт, разработанный компанией Formal Systems (Europe) Ltd. FDR2 часто описывается как средство проверки моделей , но технически это средство проверки уточнений , в том смысле, что он преобразует два выражения процесса CSP в системы меченых переходов (LTS), а затем определяет, является ли один из процессов уточнением другого в рамках некоторой указанной семантической модели (следы, сбои или сбои/расхождения). FDR2 применяет различные алгоритмы сжатия пространства состояний к процессам LTS, чтобы уменьшить размер пространства состояний, которое необходимо исследовать во время уточняющей проверки. На смену FDR2 пришла FDR3, полностью переписанная версия, включающая, помимо прочего, параллельное выполнение и встроенную проверку типов. Он выпущен Оксфордским университетом, который также выпустил FDR2 в период 2008–2012 годов.

Проверка уточнения Аделаиды ( ARC ) — это средство проверки уточнений CSP, разработанное Группой формального моделирования и проверки Университета Аделаиды . ARC отличается от FDR2 тем, что внутри он представляет процессы CSP как упорядоченные двоичные диаграммы решений (OBDD), что облегчает проблему взрыва состояний явных представлений LTS, не требуя использования алгоритмов сжатия пространства состояний, таких как те, которые используются в FDR2.

Проект ПроБ , который находится в Институте информатики Университета Генриха Гейне в Дюссельдорфе, изначально был создан для поддержки анализа спецификаций, построенных с помощью B. метода Однако он также включает поддержку анализа процессов CSP как посредством уточнения, так и LTL проверки модели . ProB также можно использовать для проверки свойств комбинированных спецификаций CSP и B. ProBE CSP Animator интегрирован в FDR3.

Набор инструментов для анализа процессов (PAT) — это инструмент анализа CSP, разработанный в Школе вычислительной техники Национального университета Сингапура . PAT может выполнять уточняющую проверку, проверку модели LTL и моделирование процессов CSP и Timed CSP. Язык процессов PAT расширяет CSP поддержкой изменяемых общих переменных, асинхронной передачи сообщений, а также различных конструкций процессов, связанных с справедливостью и количественным определением времени, таких как deadline и waituntil. Основной принцип проектирования языка процессов PAT заключается в объединении языка спецификации высокого уровня с процедурными программами (например, событием в PAT может быть последовательная программа или даже вызов внешней библиотеки C#) для большей выразительности. Изменяемые общие переменные и асинхронные каналы обеспечивают удобный синтаксический сахар для известных шаблонов моделирования процессов, используемых в стандартном CSP. Синтаксис PAT похож, но не идентичен синтаксису _M. CSP Принципиальными различиями между синтаксисом PAT и стандартным CSP _M являются использование точек с запятой для завершения выражений процесса, включение синтаксического сахара для переменных и присваиваний, а также использование немного другого синтаксиса для внутреннего выбора и параллельной композиции.

Визуальные сети создает анимированные визуализации систем CSP на основе спецификаций и поддерживает CSP с синхронизацией.

CSPsim это ленивый симулятор. Он не моделирует проверку CSP, но полезен для исследования очень больших (потенциально бесконечных) систем.

SyncStitch — это средство проверки уточнений CSP с интерактивной средой моделирования и анализа. Имеет графический редактор диаграмм переходов состояний. Пользователь может моделировать поведение процессов не только с помощью выражений CSP, но и с помощью диаграмм переходов состояний. Результаты проверки также отображаются графически в виде деревьев вычислений и могут анализироваться в интерактивном режиме с помощью периферийных инструментов проверки. В дополнение к уточняющим проверкам он может выполнять проверку взаимоблокировок и проверку работоспособности.

Связанные

Несколько других языков спецификаций и формализмов были получены из классического несинхронизированного CSP или вдохновлены им, в том числе:

• CSP по времени , который включает в себя информацию о времени для рассуждений о системах реального времени.
• Теория рецептивных процессов , специализация CSP, которая предполагает асинхронную (т. е. неблокирующую ) операцию отправки.
• КСПП
• HCSP
• TCOZ , интеграция Timed CSP и Object Z.
• Circus , интеграция CSP и Z на основе Объединяющих теорий программирования.
• CML. Архивировано 19 февраля 2020 г. в Wayback Machine (язык моделирования COMPASS), комбинации Circus и VDM , разработанной для моделирования систем систем (SoS).
• CspCASL , расширение CASL , интегрирующее CSP.
• ЛОТОС , международный стандарт который включает в себя функции CSP и CCS .
• PALPS , вероятностное расширение с местами для экологических моделей, разработанное Анной Филиппу и Маурисио Торо Бермудесом.

Сравнение с моделью актера

В том, что касается параллельных процессов, обменивающихся сообщениями, модель актера во многом похожа на CSP. Однако эти две модели делают принципиально разные выборы в отношении предоставляемых ими примитивов:

• Процессы CSP анонимны, а субъекты имеют личность.
• CSP использует явные каналы для передачи сообщений, тогда как системы субъектов передают сообщения именованным субъектам назначения. Эти подходы можно рассматривать как двойственные друг другу в том смысле, что процессы, поступающие по одному каналу, фактически имеют идентификатор, соответствующий этому каналу, в то время как связь между актерами на основе имен может быть нарушена путем создания акторов, которые ведут себя как каналы.
• Передача сообщений CSP по сути предполагает встречу между процессами, участвующими в отправке и получении сообщения, то есть отправитель не может передать сообщение до тех пор, пока получатель не будет готов его принять. Напротив, передача сообщений в актерских системах принципиально асинхронна, т.е. передача и прием сообщений не обязательно должны происходить одновременно, и отправители могут передавать сообщения до того, как получатели будут готовы их принять. Эти подходы также можно считать двойственными друг другу в том смысле, что системы на основе рандеву могут использоваться для построения буферизованных коммуникаций, которые ведут себя как асинхронные системы обмена сообщениями, в то время как асинхронные системы могут использоваться для построения коммуникаций в стиле рандеву с использованием сообщения/ протокол подтверждения для синхронизации отправителей и получателей.

Обратите внимание, что вышеупомянутые свойства не обязательно относятся к оригинальной статье CSP Хоара, а скорее к современному воплощению идеи, как это видно в таких реализациях, как Go и Clojure core.async. В исходной статье каналы не были центральной частью спецификации, а процессы отправителя и получателя фактически идентифицировали друг друга по имени.

Награда

В 1990 году « Королевская премия за технологические достижения была вручена… вычислительной лаборатории [Оксфордского университета]» . Эта награда является признанием успешного сотрудничества между лабораторией и Inmos Ltd.… Флагманским продуктом Inmos является « транспьютер », микропроцессор со многими деталями, которые обычно необходимы дополнительно, встроенными в один и тот же компонент ». По словам Тони Хоара, «INMOS Transputer был воплощением идеи… создания микропроцессоров, которые могли бы связываться друг с другом по проводам, проходящим между их терминалами. У основателя было видение, что идеи CSP созрели для промышленного использования, и он положил это в основу языка программирования транспьютеров, который получил название Occam . … По оценкам компании, это позволило им поставить оборудование на год раньше, чем это могло бы произойти в противном случае. Они подали заявку и выиграли Королевскую премию за технологические достижения совместно с вычислительной лабораторией Оксфордского университета».

См. также

• Теория следов , общая теория следов.
• Моноид трассировки и моноид истории
• Удобный язык программирования
• язык программирования XC
• VerilogCSP — это набор макросов, добавленных в Verilog HDL для поддержки связи последовательных процессов по каналам связи.
• Joyce — язык программирования, основанный на принципах CSP, разработанный Бринчом Хансеном примерно в 1989 году.
• SuperPascal — язык программирования, также разработанный Бринчом Хансеном под влиянием CSP и его более ранней работы с Джойсом .
• Ада реализует такие функции CSP, как рандеву.
• DirectShow — это видеофреймворк внутри DirectX , он использует концепции CSP для реализации аудио- и видеофильтров.
• OpenComRTOS — это официально разработанная сетецентрическая распределенная RTOS, основанная на прагматичном расширении CSP.
• Автомат ввода/вывода
• Модель параллельного программирования
• TLA+ — еще один формальный язык для моделирования и проверки параллельных систем.

Дальнейшее чтение

• Хоар, ЦАР (2004) [1985]. Коммуникация последовательных процессов . Прентис Холл Интернэшнл. ISBN  978-0-13-153271-7 .
  • Эта книга была обновлена ​​Джимом Дэвисом из вычислительной лаборатории Оксфордского университета , а новое издание доступно для загрузки в виде PDF-файла на веб-сайте using CSP .
• Роско, AW (1997). Теория и практика параллелизма . Прентис Холл . ISBN  978-0-13-674409-2 .
  • Некоторые ссылки, относящиеся к этой книге, доступны здесь . Полный текст доступен для загрузки в формате PS или PDF Билла Роско . из списка академических публикаций

Внешние ссылки

• PDF-версия книги Хоара CSP – действуют ограничения авторских прав, перед загрузкой просмотрите текст страницы.
• Аннотация CSP (китайская версия) , некоммерческий перевод и аннотационная работа, основанная на книге Прентис-Холла (1985 г.), китайской версии Чаочэня Чжоу (1988 г.) и онлайн-версии Джима Дэвиса (2015 г.).
• WoTUG , группа пользователей для систем стиля CSP и occam, содержит некоторую информацию о CSP и полезные ссылки.
• «Цитаты CSP» от CiteSeer