순차 프로세스 전달

컴퓨터 과학에서 CSP(Communicating Sequential Process)는 동시 ^[1]시스템에서의 상호작용 패턴을 설명하기 위한 공식 언어입니다.이것은 채널을 통해 전달되는 메시지에 기초한 프로세스 대수 또는 프로세스 계산으로 알려진 동시성 수학 이론의 일원입니다.CSP는 Occam 프로그래밍^[1]^[2] 언어 설계에 큰 영향을 미쳤으며 Limbo,^[3] RaftLib, Erlang,^[4] Go,^[5]^[3] Crystal 및 Clojure의 core.async와 ^[6]같은 프로그래밍 언어 설계에도 영향을 미쳤습니다.

CSP는 Tony ^[7]Hoare의 1978년 기사에서 처음 설명되었지만,^[8] 그 이후로 상당히 발전했습니다.CSP는 업계에서 T9000 트랜스푸터 ^[9]및 안전한 전자상거래 시스템 ^[10]등 다양한 시스템의 동시 측면을 특정 및 검증하기 위한 도구로서 실질적으로 적용되어 왔습니다.CSP의 이론 자체는, 실용성의 범위를 확대하는 작업(예를 들면, 다루기 쉽게 ^[11]분석할 수 있는 시스템의 규모를 늘리는 작업)을 포함한, 여전히 활발한 연구의 대상이다.

역사

1978년 Hoare의 최초 기사에 제시된 CSP 버전은 본질적으로 프로세스 미적분이라기보다는 동시 프로그래밍 언어였다.CSP의 최신 버전과는 상당히 다른 구문을 가지고 있었고 수학적으로 정의된 ^[12]의미론도 없었으며 무한 비결정론을 ^[13]나타낼 수 없었다.원래 CSP의 프로그램은 동기 메시지 전달을 통해 서로 통신하는 고정된 수의 순차적 프로세스의 병렬 구성으로 작성되었습니다.이후 버전의 CSP와 달리 각 프로세스에는 명시적인 이름이 할당되어 메시지의 발신원 또는 수신처가 의도된 송수신 프로세스의 이름을 지정함으로써 정의되었습니다.예를 들어, 프로세스

복사 = *[c:문자; west?c → east!c]

라는 이름의 프로세스에서 반복적으로 문자를 수신합니다.west이 문자를 프로세스로 전송합니다.east·병렬구성

[west::DISASSEMBLY X::동쪽 복사:조립]

이름을 할당하다west에게DISASSEMBLE과정,X에게COPY프로세스 및east에게ASSEMBLE이 세 가지 프로세스를 ^[7]동시에 실행합니다.

CSP의 오리지널 버전 발행에 이어 Hoare, Stephen Brookes 및 A. W. Roscoe는 CSP의 이론을 발전시키고 현대적이고 프로세스 대수적인 형태로 다듬었다.CSP를 프로세스 대수학으로 개발하는 데 채택된 접근방식은 Robin Milner의 커뮤니케이션 시스템 미적분 연구(CCS)와 그 반대로 영향을 받았다.CSP의 이론적인 버전은 Brookes, Hoare 및 Roscoe의 ^[14]1984년 기사에서 처음 제시되었고, 이후 Hoare의 책 Communicating Sequential Processes에서 1985년에 ^[12]출판되었습니다.Citeser에 따르면^{[citation needed]} 2006년 9월에도 이 책은 여전히 컴퓨터 사이언스 참고 자료 중 세 번째로 많이 인용되었다(표본의 특성상 신뢰할 수 없는 자료였다.CSP 이론은 Hoare의 책이 출판된 이후 몇 가지 작은 변화를 겪었다.이러한 변경의 대부분은 CSP 프로세스 분석 및 검증을 위한 자동화된 툴의 출현에 의해 이루어졌습니다.Roscoe의 The The Theory and Practice of Concurrency(동시성의^[1] 이론과 실천)는 이 새로운 버전의 CSP에 대해 설명합니다.

적용들

CSP의 초기 및 중요한 적용은 대규모 멀티프로세싱을 지원하도록 설계된 복잡한 슈퍼칼라 파이프라인 프로세서인 INMOS T9000 트랜스푸터의 사양 및 요소 검증에 사용된 것입니다.CSP는 프로세서 파이프라인과 ^[9]프로세서의 오프칩 통신을 관리하는 가상 채널 프로세서가 모두 올바른지 확인하기 위해 사용되었습니다.

소프트웨어 설계에 대한 CSP의 산업적 응용은 일반적으로 신뢰할 수 있고 안전에 중요한 시스템에 초점을 맞추고 있습니다.예를 들어 브레멘 세이프 시스템 연구소(Institute for Safe Systems)와 다임러-벤츠 에어로스페이스(Daimler-Benz Aerospace)는 CSP의 국제우주정거장에서 사용하기 위한 고장관리시스템과 항전 인터페이스(약 23,000줄로 구성)를 모델링하고 이 모델을 분석하여 교착상태와 ^[15]^[16]라이브록이 없음을 확인하였습니다.모델링 및 분석 프로세스에서는 테스트만으로는 탐지하기 어려웠던 많은 오류를 발견할 수 있었습니다.마찬가지로 Praxis High Integrity Systems는 안전한 스마트 카드 인증 기관을 위해 소프트웨어(약 10만 줄의 코드) 개발 중에 CSP 모델링 및 분석을 적용하여 설계가 안전하고 교착 상태가 없음을 검증했습니다.Praxis는 이 시스템이 유사한 시스템보다 ^[10]결점 비율이 훨씬 낮다고 주장합니다.

CSP는 복잡한 메시지 교환을 포함하는 시스템을 모델링하고 분석하는 데 적합하기 때문에 통신 및 보안 프로토콜 검증에도 적용되어 왔습니다.이러한 종류의 어플리케이션의 대표적인 예로는 Lowe가 CSP와 FDR 미세 체커를 사용하여 Needham-Schroeder 공개키 인증 프로토콜에 대해 이전에 알려지지 않았던 공격을 검출하고 공격을 ^[17]물리칠 수 있는 수정된 프로토콜을 개발하는 것입니다.

비공식적인 설명

이름에서 알 수 있듯이 CSP는 독립적으로 작동하고 메시지 전달 통신만을 통해 상호 작용하는 컴포넌트 프로세스의 관점에서 시스템을 기술할 수 있습니다.그러나 현대의 CSP에서는 컴포넌트 프로세스를 순차 프로세스와 보다 원시적인 프로세스의 병렬 구성으로 정의할 수 있기 때문에 CSP 이름의 "시퀀셜" 부분은 잘못된 명칭이 되었습니다.서로 다른 프로세스 간의 관계와 각 프로세스가 환경과 통신하는 방법은 다양한 프로세스 대수 연산자를 사용하여 설명합니다.이 대수적 접근법을 사용하면 몇 가지 원시 요소에서 상당히 복잡한 프로세스 기술을 쉽게 구성할 수 있습니다.

원어민

CSP는 프로세스 대수에서 다음 두 가지 기본 클래스를 제공합니다.

이벤트: 이벤트는 통신 또는 상호작용을 나타냅니다.그것들은 분리될 수 없고 순간적인 것으로 가정된다.원자 이름(예: on, off), 복합 이름(예: valve.open, valve.close) 또는 입력/출력 이벤트(예: mouse?xy, screen!bitmap)일 수 있습니다.
원시 과정: 원시 프로세스는 기본 동작을 나타냅니다.예를 들어 STOP(아무것도 통신하지 않는 프로세스, 데드록이라고도 함) 및 SKIP(정상적인 종료를 나타냄)가 있습니다.

대수 연산자

CSP에는 광범위한 대수 연산자가 있습니다.주요 항목은 다음과 같습니다.

프리픽스: 프리픽스 연산자는 이벤트와 프로세스를 결합하여 새로운 프로세스를 생성합니다.예를들면,

a\to P

는, 그 환경과

통신

하려고 하는 프로세스이며, 그

후

에는

프로세스

P와 같이 동작합니다.

결정론적 선택: 결정론적(또는 외부) 선택 연산자는 프로세스의 미래 진화를 2개의 컴포넌트 프로세스 중 하나의 초기 이벤트를 전달하여 선택 사항을 해결할 수 있도록 합니다.예를들면,

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

는 초기

이벤트a

와

b 의 통신을 실시해, 그 후에 환경이

통신

하도록 선택하는 초기

이벤트

에 따라, P 또는 Q 로서 동작하는 프로세스입니다.

a

와 b가

동시

에 통신되는 경우 선택은 비결정적으로 해결됩니다.

비결정적 선택: 비결정론적(또는 내부) 선택 연산자는 프로세스의 미래 진화를 두 가지 구성 요소 프로세스 간의 선택으로 정의할 수 있지만 환경에서는 어떤 구성 요소 프로세스가 선택될지에 대한 제어는 허용하지 않습니다.예를들면,

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

는 (

(a\to P)

(a\to P)

) {

displaystyle (a\to

P

)}

또는

(a\to P)

(b\to Q)

(

(b\to Q)

)

{

displaystyle (b\to

Q

(b\to Q)

과

(a\to P)

같이 동작할 수 있습니다.a

또는

b의

수신

을 거부할 수 있으며, 환경이

a

와 b를 모두

제공

하는 경우에만 통신할 의무가 있습니다.선택 양쪽의 초기 사건이 동일할 경우, 비결정론이 명목상 결정론적 선택에 무심코 도입될 수 있다.예를 들어,

\displaystyle(a\to\text)STOP})\Box(a에서 b로)\text{STOP}}}}:

와 동등하다

a에서 big (a)로 (a에서 text로) 표시STOP})\sqcap(b\text{)STOP}){\big}}}

인터리빙: 인터리브 연산자는 완전히 독립된 동시 액티비티를 나타냅니다.프로세스

P\;\;Q

는 P와

Q

로

동시

에 동작합니다.두 프로세스에서 발생하는 이벤트는 시간 내에 임의로 인터리브됩니다.

인터페이스 병렬: 인터페이스 병렬 연산자는 컴포넌트 프로세스 간의 동기화가 필요한 동시 액티비티를 나타냅니다.인터페이스 세트의 이벤트는 모든 컴포넌트 프로세스가 해당 이벤트에 참여할 수 있는 경우에만 발생합니다.예를 들어, 프로세스

P\; [\{a\}\;Q

그럼 이벤트가 발생하기 전에 P와

Q

가 모두

이벤트

를 실행할 수

있어야

합니다.예를 들어, 이 프로세스는

(a\to P)\; [\{a\} \;(a\to Q)

이벤트

a에 관여하여 프로세스가 될 수 있다

P\; [\{a\}\;Q

하는 동안에

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

그냥 교착상태에 빠집니다.

숨기다: 숨김 연산자는 일부 이벤트를 관찰할 수 없도록 함으로써 프로세스를 추상화하는 방법을 제공합니다.숨김의 간단한 예는 다음과 같습니다.

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

이벤트

a가 P에

표시

되지 않는다고 가정하면 단순히 로 감소합니다.

P

예

전형적인 CSP의 예 중 하나는 초콜릿 자판기와 초콜릿을 사고 싶어하는 사람과의 상호작용을 추상적으로 표현한 것입니다.이 자판기는 각각 결제와 초콜릿 배달의 두 가지 다른 이벤트인 "코인"과 "척"을 진행할 수 있을 것이다.초콜릿을 제공하기 전에 지불(현금만)을 요구하는 기계는 다음과 같이 쓸 수 있습니다.

\displaystyle \mathrm {Vending Machine} = \mathrm {coin} \rightarrow {choc} \rightarrow \mathrm {STOP}

코인 또는 카드를 사용하여 결제하는 사람은 다음과 같이 모델링할 수 있습니다.

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

이 두 프로세스를 병렬로 배치하여 상호 작용할 수 있습니다.복합 프로세스의 동작은 두 구성 요소 프로세스가 동기화해야 하는 이벤트에 따라 달라집니다.따라서,

\displaystyle \mathrm {Vending Machine} \left \vert \left [ \ mathrm { coin } , \ mathrm { coin } \ right \ vert \ mathrm { person } \ equiv \ mathrm { coin } \ right \ arrow \ mathrm { sTOP }

동기가 "코인"에서만 필요한 경우,

\displaystyle \mathrm {Vending Machine} \left [\left\{\mathrm {coin}\right\vert\mathrm {Person}\equiv \left(\mathrm {coin}\rightarrow {choc} \rightarrow \m {STOP}\right}\right)상자 \left(\mathrm {card} \right 화살표 \mathrm {STOP} \right)}

"코인"과 "카드" 이벤트를 숨김으로써 후자의 복합 프로세스를 추상화하면 다음과 같습니다.

\displaystyle \left(\mathrm {coin}\rightarrow \mathrm {choc}\rightarrow \mathrm {STOP}\right)\상자 \left(\mathrm {card} \right 화살표 \mathrm {STOP} \right)\setminus \left\{\mathrm {coin, card} \right\})

우리는 비결정적인 과정을 거친다

\displaystyle \left(\mathrm {choc} \right 화살표 \mathrm {STOP} \right)\sqcap \mathrm {STOP}

이는 "초크" 이벤트를 제공한 후 중지하거나 중지하는 프로세스입니다.즉, 추상화를 시스템의 외부 견해(예를 들어, 개인이 도달한 결정을 보지 못하는 사람)로 취급한다면, 비결정론이 도입되었다.

형식적 정의

구문

CSP의 구문은 프로세스와 이벤트를 결합할 수 있는 "합법적인" 방법을 정의합니다.e를 이벤트로 $하고$ X를 일련의 이벤트로 $합니다$ .다음으로 CSP의 기본 구문을 다음과 같이 정의할 수 있습니다.

{\displaystyle\begin{array}{lcll}{Proc}&:=&,\mathrm{정지}&\;\\&,&\mathrm{스킵}&\;\\&,&e\rightarrow{Proc}&,({\text{고정 영역 변환}})\\&,&.{Proc}\, \Box.{Proc}&,({{}외부}\,{\text{선택}\text})\\&,&\와 같이{Proc}\, \sqcap,{Proc}&,({\text{}비결정론적인}\,{\text{선택}})\\&,&{Proc}\, \vert \vert\vert\;{Proc}&,({\text{}인터리빙})\\&,&.{Proc}\,[){X\}]);{Proc}&.({\text{인터페이스}}\,{\text{구 유고 슬라비아의 화폐 단위llel})\&{Proc}\setminus X&({\text{hiding}})\&{Proc};{Proc}&({\text{sequential}\;{\text{composition}})\&\mathrm {if}\;b\;\mathrm {else}\;Proc&({\text{boolan}}\;{\text{condition}}\\\\c}\\\\\mathrm {triang}\c}\\c}\\\\\c}\&{Proc}\;\triangle\;{Proc}&({\text{interrupt}})\end{array}}

간결하게 하기 위해 위의 구문에서는 $\mathbf {div}$ v \ $displaystyle$ \ $mathbf$ {div $}$ $\mathbf {div}$ 와 $\mathbf {div}$ 알파벳 순으로 정렬된 병렬, 배관 및 색인화된 선택과 같은 다양한 연산자가 제외됩니다.

형식 의미론

CSP에는 구문적으로 올바른 CSP 표현의 의미를 정의하는 몇 가지 다른 형식적 의미가 포함되어 있습니다.CSP의 이론은 상호 일관된 표현적 의미론, 대수적 의미론 및 운영적 의미론을 포함한다.

표기 의미론

CSP의 세 가지 주요 표현 모델은 추적 모델, 안정적인 고장 모델 및 고장/분산 모델입니다.프로세스 표현식에서 이들 3가지 모델 각각에 대한 의미적 매핑은 ^[1]CSP에 대한 표현적 의미론을 제공합니다.

트레이스 모델은 프로세스 식의 의미를 프로세스가 수행하도록 관찰할 수 있는 일련의 이벤트(추적)로 정의합니다.예를들면,

$\mathrm {traces} \left(\mathrm {STOP} \right)=\left\{\langle \rangle \right\}$ $\mathrm {STOP}$ $\mathrm {STOP}$ $\mathrm {STOP}$ $\mathrm {traces} \left(\mathrm {STOP} \right)=\left\{\langle \rangle \right\}$ s ( $\mathrm {traces} \left(\mathrm {STOP} \right)=\left\{\langle \rangle \right\}$ $\mathrm {traces} \left(\mathrm {STOP} \right)=\left\{\langle \rangle \right\}$ $\mathrm {traces} \left(\mathrm {STOP} \right)=\left\{\langle \rangle \right\}$ ) $=$ { $\mathrm {traces} \left(\mathrm {STOP} \right)=\left\{\langle \rangle \right\}$ $}$ { $displaystyle$ \ $mathrm { sTOP }$ \ $left$ ( \ $mathrm$ { $STOP$ $}$ \ $right$ )= \ $left$ \ { \ $right$ \ $\mathrm {traces} \left(\mathrm {STOP} \right)=\left\{\langle \rangle \right\}$ { \ $displaystyle \ mathrm { STOP }$ }이벤트를 $\mathrm {traces} \left(\mathrm {STOP} \right)=\left\{\langle \rangle \right\}$ $\mathrm {STOP}$ 실행하지 $\mathrm {STOP}$ .
$\mathrm {traces} \left(a\rightarrow b\rightarrow \mathrm {STOP} \right)=\left\{\langle \rangle ,\langle a\rangle ,\langle a,b\rangle \right\}$ $\mathrm {traces} \left(a\rightarrow b\rightarrow \mathrm {STOP} \right)=\left\{\langle \rangle ,\langle a\rangle ,\langle a,b\rangle \right\}$ $\mathrm {traces} \left(a\rightarrow b\rightarrow \mathrm {STOP} \right)=\left\{\langle \rangle ,\langle a\rangle ,\langle a,b\rangle \right\}$ $\mathrm {traces} \left(a\rightarrow b\rightarrow \mathrm {STOP} \right)=\left\{\langle \rangle ,\langle a\rangle ,\langle a,b\rangle \right\}$ s ( a $\mathrm {traces} \left(a\rightarrow b\rightarrow \mathrm {STOP} \right)=\left\{\langle \rangle ,\langle a\rangle ,\langle a,b\rangle \right\}$ $\mathrm {traces} \left(a\rightarrow b\rightarrow \mathrm {STOP} \right)=\left\{\langle \rangle ,\langle a\rangle ,\langle a,b\rangle \right\}$ $\mathrm {traces} \left(a\rightarrow b\rightarrow \mathrm {STOP} \right)=\left\{\langle \rangle ,\langle a\rangle ,\langle a,b\rangle \right\}$ $\mathrm {traces} \left(a\rightarrow b\rightarrow \mathrm {STOP} \right)=\left\{\langle \rangle ,\langle a\rangle ,\langle a,b\rangle \right\}$ $\mathrm {traces} \left(a\rightarrow b\rightarrow \mathrm {STOP} \right)=\left\{\langle \rangle ,\langle a\rangle ,\langle a,b\rangle \right\}$ $\mathrm {traces} \left(a\rightarrow b\rightarrow \mathrm {STOP} \right)=\left\{\langle \rangle ,\langle a\rangle ,\langle a,b\rangle \right\}$ P $\mathrm {traces} \left(a\rightarrow b\rightarrow \mathrm {STOP} \right)=\left\{\langle \rangle ,\langle a\rangle ,\langle a,b\rangle \right\}$ ) $\mathrm {traces} \left(a\rightarrow b\rightarrow \mathrm {STOP} \right)=\left\{\langle \rangle ,\langle a\rangle ,\langle a,b\rangle \right\}$ { $\mathrm {traces} \left(a\rightarrow b\rightarrow \mathrm {STOP} \right)=\left\{\langle \rangle ,\langle a\rangle ,\langle a,b\rangle \right\}$ a $\mathrm {traces} \left(a\rightarrow b\rightarrow \mathrm {STOP} \right)=\left\{\langle \rangle ,\langle a\rangle ,\langle a,b\rangle \right\}$ 、 $\mathrm {traces} \left(a\rightarrow b\rightarrow \mathrm {STOP} \right)=\left\{\langle \rangle ,\langle a\rangle ,\langle a,b\rangle \right\}$ , $\mathrm {traces} \left(a\rightarrow b\rightarrow \mathrm {STOP} \right)=\left\{\langle \rangle ,\langle a\rangle ,\langle a,b\rangle \right\}$ 、 a $\mathrm {traces} \left(a\rightarrow b\rightarrow \mathrm {STOP} \right)=\left\{\langle \rangle ,\langle a\rangle ,\langle a,b\rangle \right\}$ 、 b 、 b ⟩} $\mathrm {traces} \left(a\rightarrow b\rightarrow \mathrm {STOP} \right)=\left\{\langle \rangle ,\langle a\rangle ,\langle a,b\rangle \right\}$ \ $displaystyle$ \ $mathrm { rightarrow b$ \ $rightarrow$ { STOP } \ $right$ = \ left \ $rangle$ \ rangle , $rangle$ , $rangle$ , rangle , $rangle$ , rangle , rangle , 。n 이벤트, $이벤트$ a 또는 일련의 $이벤트$ $a$ 에 이어 b를 수행하지 않은 것으로 관찰된다.

보다 형식적으로 트레이스 모델에서의 $프로세스P$ 의 의미는 다음과 같이 t $\mathrm {traces} \left(P\right)\subseteq \Sigma ^{\ast }$ $\mathrm {traces} \left(P\right)\subseteq \Sigma ^{\ast }$ c $\mathrm {traces} \left(P\right)\subseteq \Sigma ^{\ast }$ ( $\mathrm {traces} \left(P\right)\subseteq \Sigma ^{\ast }$ $\mathrm {traces} \left(P\right)\subseteq \Sigma ^{\ast }$ {\ {\ {\ $、$ \ $displaystyle$ \ $mathrm$ { $traces$ } \ $left$ ( $P$ \ $right$ ) \ $subseteq$ \ $Sigma$ ^ { \ { \ $ast$ } 로 $\mathrm {traces} \left(P\right)\subseteq \Sigma ^{\ast }$ 됩니다.

$\langle \rangle \in \mathrm {traces} \left(P\right)$ $\langle \rangle \in \mathrm {traces} \left(P\right)$ ( $\langle \rangle \in \mathrm {traces} \left(P\right)$ ) \ $displaystyle$ \ $langle$ \ $in$ \ $mathrm$ { $traces$ } \ $left$ ( P \ $\langle \rangle \in \mathrm {traces} \left(P\right)$ right $\langle \rangle \in \mathrm {traces} \left(P\right)$ ) （ $\mathrm {traces} \left(P\right)$ a $\mathrm {traces} \left(P\right)$ s ( $\mathrm {traces} \left(P\right)$ ) \ $displaystyle$ \ $mathrm$ { $traces$ } \ $left$ ( P \ $right$ ) ） $\langle \rangle \in \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)$ 1 $s_{1}\smallfrown s_{2}\in \mathrm {traces} \left(P\right)\implies s_{1}\in \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)$ 2 $s_{1}\smallfrown s_{2}\in \mathrm {traces} \left(P\right)\implies s_{1}\in \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)$ $s_{1}\smallfrown s_{2}\in \mathrm {traces} \left(P\right)\implies s_{1}\in \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)$ $s_{1}\smallfrown s_{2}\in \mathrm {traces} \left(P\right)\implies s_{1}\in \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)$ ( P $s_{1}\smallfrown s_{2}\in \mathrm {traces} \left(P\right)\implies s_{1}\in \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)$ $s_{1}\smallfrown s_{2}\in \mathrm {traces} \left(P\right)\implies s_{1}\in \mathrm {traces} \left(P\right)$ a c $s_{1}\smallfrown s_{2}\in \mathrm {traces} \left(P\right)\implies s_{1}\in \mathrm {traces} \left(P\right)$ s $s_{1}\smallfrown s_{2}\in \mathrm {traces} \left(P\right)\implies s_{1}\in \mathrm {traces} \left(P\right)$ ( P $s_{1}\smallfrown s_{2}\in \mathrm {traces} \left(P\right)\implies s_{1}\in \mathrm {traces} \left(P\right)$ ) \ $displaystyle s_{$ 1} \ $smallfrown s_{$ 2} \ $in$ \ $mathrm$ { $traces$ } \ $implies s_{1}$ \ $in$ \ $in$ \ in \ $mathrm$ { $traces （ P\ right$ } $s_{1}\smallfrown s_{2}\in \mathrm {traces} \left(P\right)\implies s_{1}\in \mathrm {traces} \left(P\right)$ \ i ）

여기서 $\Sigma ^{\ast }$ ${\$ \ $displaystyle$ \ $Sigma$ ^ { \ $ast$ } $\Sigma ^{\ast }$ is $\Sigma ^{\ast }$ 、 가능한 모든 유한 이벤트시퀀스의 세트입니다.

안정적인 장애 모델은 프로세스에서 실행을 거부할 수 있는 $X\subseteq \Sigma$ X $X\subseteq \Sigma$ 인 $X\subseteq \Sigma$ 거부 세트를 사용하여 트레이스 모델을 확장합니다.거부 세트는 X " $X\subseteq \Sigma$ "\ $displaystyle$ X $\subseteq \Sigma$ } $。$ 장애란 $트레이스$ 및 $프로세스$ 가 트레이스를 실행한 후 거부할 가능성이 있는 이벤트를 식별하는 $거부$ 세트X로 구성된 $\left(s,X\right)$ 쌍 ( $\left(s,X\right)$ , $\left(s,X\right)$ ) $\left(s,X\right)$ \ $displaystyle \left ( s$ , $X$ \ $right$ )안정된 장애 모델에서의 프로세스의 동작은 쌍 $\left(\mathrm {traces} \left(P\right),\mathrm {failures} \left(P\right)\right)$ $\left(\mathrm {traces} \left(P\right),\mathrm {failures} \left(P\right)\right)$ $\left(\mathrm {traces} \left(P\right),\mathrm {failures} \left(P\right)\right)$ $\left(\mathrm {traces} \left(P\right),\mathrm {failures} \left(P\right)\right)$ $\left(\mathrm {traces} \left(P\right),\mathrm {failures} \left(P\right)\right)$ ( $\left(\mathrm {traces} \left(P\right),\mathrm {failures} \left(P\right)\right)$ $\left(\mathrm {traces} \left(P\right),\mathrm {failures} \left(P\right)\right)$ $\left(\mathrm {traces} \left(P\right),\mathrm {failures} \left(P\right)\right)$ $\left(\mathrm {traces} \left(P\right),\mathrm {failures} \left(P\right)\right)$ $\left(\mathrm {traces} \left(P\right),\mathrm {failures} \left(P\right)\right)$ r $\left(\mathrm {traces} \left(P\right),\mathrm {failures} \left(P\right)\right)$ s ( $),$ \style $\left$ ( \ $mathrm$ { $traces$ } \ $left$ ( P \ right $),$ \ $mathrm$ { $failures$ \ $left$ ( $P$ \ right $\left(\mathrm {traces} \left(P\right),\mathrm {failures} \left(P\right)\right)$ ) )로 설명됩니다.예를 들어,

$\displaystyle \mathrm {failures} \left(\left(a\right 화살표\mathrm {STOP}\right)\상자 \left(b\rightarrow \mathrm {STOP} \right)=\left(\left(\left \rangle,\emptyset \right),\left(\left\right\right),\left(\right(\right)\left(\right(\right(\right(\right)\left(\rangle a\rangle a\rangle a\rangle,\rangle,\rangle,\rangle,\rangle,\rangle,\$
$\displaystyle \mathrm {right} \left(\left(\right 화살표 \mathrm {STOP} \right)\cap \left(b\right 화살표 \mathrm {STOP} \right)=\left\{\left(\left\right\right\right}\right)\right(\left)\left(\left(\light)\left(\right)\light)\light(\light)\right(\right(\right)\$

고장/분산 모형은 분산을 처리하기 위해 고장 모형을 더욱 확장합니다.failures/diverses 모델에서 프로세스의 의미는 쌍 $\left(\mathrm {failures} _{\perp }\left(P\right),\mathrm {divergences} \left(P\right)\right)$ i $\left(\mathrm {failures} _{\perp }\left(P\right),\mathrm {divergences} \left(P\right)\right)$ r $\left(\mathrm {failures} _{\perp }\left(P\right),\mathrm {divergences} \left(P\right)\right)$ s $\left(\mathrm {failures} _{\perp }\left(P\right),\mathrm {divergences} \left(P\right)\right)$ ( $\left(\mathrm {failures} _{\perp }\left(P\right),\mathrm {divergences} \left(P\right)\right)$ ), $\left(\mathrm {failures} _{\perp }\left(P\right),\mathrm {divergences} \left(P\right)\right)$ $\left(\mathrm {failures} _{\perp }\left(P\right),\mathrm {divergences} \left(P\right)\right)$ e $\left(\mathrm {failures} _{\perp }\left(P\right),\mathrm {divergences} \left(P\right)\right)$ $\left(\mathrm {failures} _{\perp }\left(P\right),\mathrm {divergences} \left(P\right)\right)$ $\left(\mathrm {failures} _{\perp }\left(P\right),\mathrm {divergences} \left(P\right)\right)$ $\left(\mathrm {failures} _{\perp }\left(P\right),\mathrm {divergences} \left(P\right)\right)$ ( $){$ $displaystyle \left$ ( \ $mathrm$ { $failures } _$ { \ $left ( P$ \ $right$ ) $\left(\mathrm {failures} _{\perp }\left(P\right),\mathrm {divergences} \left(P\right)\right)$ } , \ $mathrm$ { $divergences$ } \ ） \ 。 $P\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\}$ $\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\}$ $\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\}$ r $\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\}$ $（$ P ） $\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\}$ $\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\}$ $\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\}$ $\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\}$ $\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\}$ $\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\}$ ( $\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\}$ ) $\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\}$ { $\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\}$ ( $\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\}$ s , $\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\}$ ) $\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\}$ $\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\}$ $\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\}$ $\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\}$ $\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\}$ $\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\}$ n c $\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\}$ ( P ) $}$ \ $style$ \ $mathrm$ { p $\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\}$ } \ $p$ 。 $rm {divergences}$ \ $left(P\right)\right$

도구들

수년간 CSP를 사용하여 기술된 시스템을 분석하고 이해하기 위한 수많은 도구가 생산되었습니다.초기 도구 구현에서는 CSP에 대해 기계에서 읽을 수 있는 다양한 구문을 사용했기 때문에 서로 다른 도구에 대해 작성된 입력 파일이 호환되지 않았습니다.그러나 현재 대부분의 CSP 툴은 Bryan Sactergood가 고안한 CSP의 기계 판독 가능한 방언(CSP라고도 함)^[18]으로_M 표준화되어 있습니다.CSP의 CSP 방언은_M 공식적으로 정의된 운영 의미론을 가지고 있으며, 여기에는 내장된 기능 프로그래밍 언어가 포함됩니다.

가장 잘 알려진 CSP 툴은 FDR2(Failures/Divergence Refinement 2)일 것입니다.FDR2는 Formal Systems(European) Ltd가 개발한 상용제품입니다.FDR2는 모델 체커로 기술되어 있지만 기술적으로는 2개의 CSP 프로세스식을 라벨이 붙은 시스템(Transition Systems)으로 변환하고 있습니다.ether 프로세스 중 하나는 지정된 의미 모델(장애, 장애 또는 장애/컨버전스)^[19] 내에서 다른 프로세스를 개량한 것입니다.FDR2는 프로세스 LTS에 다양한 상태 공간 압축 알고리즘을 적용하여 미세화 검사 중에 조사해야 하는 상태 공간의 크기를 줄입니다.FDR2는 병렬 실행 및 통합형 검사 기능을 통합한 완전히 다시 작성된 버전인 FDR3에 의해 계승되었습니다.그것은 옥스포드 대학에 의해 발표되었고, 옥스포드 대학도 2008년에서 ^[20]2012년 사이에 FDR2를 출시했다.

애들레이드 미세화 검사기(ARC)^[21]는 애들레이드 대학의 공식 모델링 및 검증 그룹이 개발한 CSP 미세화 검사기입니다.ARC는 내부적으로 CSP 프로세스를 Ordered Binary Decision Diagram(OBDD; 오더 바이너리 결정도)로 나타낸다는 점에서 FDR2와 다릅니다.이것에 의해, FDR2에 사용되는 상태 공간 압축 알고리즘을 사용하지 않아도, 명시적인 LTS 표현의 상태 폭발 문제가 경감됩니다.

Heinrich-Heine-Universitét Dusseldorf의 Institut für Informatik 주최 ProB ^[22]프로젝트는 원래 B 방식으로 구성된 사양 분석을 지원하기 위해 만들어졌습니다.그러나 정제 검사와 LTL 모델 검사를 통해 CSP 프로세스의 분석을 지원하는 것도 포함됩니다.ProB는 CSP와 B 규격의 결합 속성을 확인하는 데도 사용할 수 있습니다.ProBE CSP 애니메이터는 FDR3에 내장되어 있습니다.

Process Analysis Toolkit(PAT)은 싱가포르 국립대학교 컴퓨팅대학에서 개발된 CSP 분석 도구입니다.PAT는 정밀도 검사, LTL 모델 검사 및 CSP 및 타이밍 설정 CSP 프로세스의 시뮬레이션을 수행할 수 있습니다.PAT 프로세스 언어는 가변 공유 변수, 비동기 메시지 전달 및 다음과 같은 다양한 공정성 및 양적 시간 관련 프로세스 구조를 지원하여 CSP를 확장합니다.deadline그리고.waituntilPAT 프로세스 언어의 기본 설계 원칙은 높은 수준의 사양 언어를 절차 프로그램과 결합하는 것입니다(예를 들어 PAT 내의 이벤트는 순차적인 프로그램 또는 외부 C# 라이브러리 호출일 수 있습니다).가변 공유 변수와 비동기 채널은 표준 CSP에서 사용되는 잘 알려진 프로세스 모델링 패턴에 편리한 통사당을 제공합니다.PAT 구문은 ^[25]CSP와_M 비슷하지만 동일하지는 않습니다.PAT 구문과 표준_M CSP의 주요 차이점은 프로세스 식을 종료하기 위한 세미콜론 사용, 변수 및 할당에 구문설탕 포함, 내부 선택 및 병렬 구성에 약간 다른 구문 사용입니다.

VisualNets는^[26] 사양에서 CSP 시스템의 애니메이션 시각화를 제작하고 시간 지정 CSP를 지원합니다.

CSPSim은^[27] 게으른 시뮬레이터입니다.CSP를 모델화하지는 않지만 매우 큰(잠재적으로 무한) 시스템을 탐색하는 데 유용합니다.

SyncStitch는 대화형 모델링 및 분석 환경을 갖춘 CSP 미세 검사기입니다.그래픽 상태 전이 다이어그램 편집기가 있습니다.사용자는 프로세스의 동작을 CSP 식뿐만 아니라 상태 전이 다이어그램으로 모델링할 수 있습니다.체크 결과는 계산 트리로 그래픽으로 보고되며 주변 검사 도구를 사용하여 대화식으로 분석할 수 있습니다.미세조회뿐만 아니라 교착조회, 라이브락체크도 할 수 있습니다.

배우 모델과의 비교

메시지를 교환하는 동시 프로세스에 관한 한 액터 모델은 CSP와 대체로 유사합니다.그러나 두 모델은 기본적으로 제공되는 기본 요소와 관련하여 몇 가지 다른 선택을 합니다.

CSP 프로세스는 익명으로 진행되며, 액터는 아이덴티티를 가집니다.
CSP는 메시지 전달에 명시적인 채널을 사용하는 반면 액터 시스템은 지정된 수신처 액터에게 메시지를 전송합니다.이러한 접근법은 단일 채널을 통해 수신하는 프로세스가 효과적으로 그 채널에 대응하는 식별성을 갖는다는 점에서 서로의 이중으로 간주될 수 있으며, 반면 행위자 간의 이름 기반 결합은 채널로 동작하는 행위자를 구성함으로써 깨질 수 있다.
CSP 메시지 전달은 기본적으로 메시지 송수신에 관련된 프로세스 간의 랑데부(rendezvous)를 수반합니다.즉, 송신자는 수신자가 메시지를 수신할 준비가 될 때까지 메시지를 송신할 수 없습니다.이와는 대조적으로, 행위자 시스템에서 메시지 전달은 기본적으로 비동기적이다. 즉, 메시지 송수신이 동시에 발생할 필요가 없으며, 송신자는 수신자가 메시지를 수신할 준비가 되기 전에 메시지를 전송할 수 있다.이러한 접근법은 또한 랑데부 기반 시스템이 비동기 메시징 시스템으로서 동작하는 버퍼링된 통신을 구축하는 데 사용될 수 있는 반면, 비동기 시스템은 메시지/확인 프로토콜을 사용하여 송신자를 동기화함으로써 랑데부 스타일의 통신을 구축하는 데 사용될 수 있다는 점에서 서로의 이중으로 간주될 수 있다.및 리시버

상기 속성은 반드시 Hoare의 CSP 원본을 참조하는 것이 아니라 Golang 및 Clojure의 core.async와 같은 구현에서 볼 수 있는 아이디어의 현대적 화신임을 유의하십시오.원본 문서에서는 채널이 사양의 중심 부분이 아니었으며, 송신자와 수신자 프로세스는 실제로 서로를 이름으로 식별합니다.

상

1990년에는 '기술공로상 여왕상'이 수여되었습니다.[Oxford University] Computing Laboratory에 있습니다.이 상은 연구소와 Inmos Ltd. 간의 성공적인 협업을 인정합니다. Inmos의 주력 제품은 '트랜스푸터'로, 일반적으로 필요한 많은 ^[29]부품을 동일한 단일 컴포넌트에 내장하고 있습니다."Tony Hoare에 ^[30]따르면, "INMOS Transputer는 단자를 연결하는 와이어를 통해 서로 통신할 수 있는 마이크로프로세서를 구축하는 아이디어의 구현이었습니다.설립자는 CSP 아이디어가 산업용 개발에 적합하다는 비전을 가지고 있으며, Occam이라고 불리는 트랜스푸터를 프로그래밍하기 위한 언어의 기초를 만들었습니다.…당사에서는, 그 외의 경우보다 1년 빨리 하드웨어를 제공할 수 있었다고 추정했습니다.그들은 옥스포드 대학 컴퓨터 연구소와 공동으로 기술 업적에 대한 퀸 상을 신청했고 수상했습니다."

「」를 참조해 주세요.

추적 이론, 추적의 일반 이론입니다.
트레이스 모노이드 및 이력 모노이드
쉬운 프로그래밍 언어
XC 프로그래밍 언어
VerilogCSP는 순차 프로세스 채널 통신을 지원하기 위해 Verilog HDL에 추가된 매크로 세트입니다.
조이스는 1989년경 브린치 한센에 의해 개발된 CSP의 원리에 기초한 프로그래밍 언어입니다.
SuperPascal은 브린치 한센에 의해 개발된 프로그래밍 언어이며 CSP와 조이스의 초기 작업에 영향을 받았습니다.
Ada는 랑데부 등의 CSP 기능을 구현합니다.
DirectShow는 DirectX 내의 비디오 프레임워크이며 CSP 개념을 사용하여 오디오 및 비디오 필터를 구현합니다.
OpenComRTOS는 CSP의 실용적인 슈퍼셋을 기반으로 정식으로 개발된 네트워크 중심의 분산 RTOS입니다.
입출력 자동화
병렬 프로그래밍 모델

레퍼런스

^ ^a ^b ^c ^d Roscoe, A. W. (1997). The Theory and Practice of Concurrency (PDF). Prentice Hall. ISBN 978-0-13-674409-2.
^ Inmos (1995-05-12). occam 2.1 Reference Manual (PDF). SGS-THOMSON Microelectronics Ltd., INMOS 문서 72 oc 45 03.
^ ^a ^b Cox, Russ. "Bell Labs and CSP Threads". Retrieved 2010-04-15.
^ "10 Academic and Historical Questions". Retrieved 2021-11-15.
^ "FAQ: Why build concurrency on the ideas of CSP?". The Go Programming Language. Retrieved 2021-10-15.
^ Hickey, Rich (2013-06-28). "Clojure core.async Channels". Retrieved 2021-10-15.
^ ^a ^b Hoare, C. A. R. (1978). "Communicating sequential processes". Communications of the ACM. 21 (8): 666–677. doi:10.1145/359576.359585. S2CID 849342.
^ Abdallah, Ali E.; Jones, Cliff B.; Sanders, Jeff W. (2005). Communicating Sequential Processes: The First 25 Years. LNCS. Vol. 3525. Springer. ISBN 9783540258131.
^ ^a ^b Barrett, G. (1995). "Model checking in practice: The T9000 Virtual Channel Processor". IEEE Transactions on Software Engineering. 21 (2): 69–78. doi:10.1109/32.345823.
^ ^a ^b Hall, A; Chapman, R. (2002). "Correctness by construction: Developing a commercial secure system" (PDF). IEEE Software. 19 (1): 18–25. CiteSeerX 10.1.1.16.1811. doi:10.1109/52.976937.
^ Creese, S. (2001). Data Independent Induction: CSP Model Checking of Arbitrary Sized Networks (D. Phil.). Oxford University. CiteSeerX 10.1.1.13.7185.
^ ^a ^b Hoare, C. A. R. (1985). Communicating Sequential Processes. Prentice Hall. ISBN 978-0-13-153289-2.
^ Clinger, William (June 1981). Foundations of Actor Semantics (Mathematics Doctoral Dissertation). MIT. hdl:1721.1/6935.
^ Brookes, Stephen; Hoare, C. A. R.; Roscoe, A. W. (1984). "A Theory of Communicating Sequential Processes". Journal of the ACM. 31 (3): 560–599. doi:10.1145/828.833. S2CID 488666.
^ Buth, B.; M. Kouvaras; J. Peleska; H. Shi (December 1997). "Deadlock analysis for a fault-tolerant system". Proceedings of the 6th International Conference on Algebraic Methodology and Software Technology (AMAST’97). pp. 60–75.
^ Buth, B.; J. Peleska; H. Shi (January 1999). "Combining methods for the livelock analysis of a fault-tolerant system". Proceedings of the 7th International Conference on Algebraic Methodology and Software Technology (AMAST’98). pp. 124–139.
^ Lowe, G. (1996). "Breaking and fixing the Needham–Schroeder public-key protocol using FDR". Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer-Verlag. pp. 147–166.
^ Scattergood, J.B. (1998). "The Semantics and Implementation of Machine-Readable CSP". D.Phil. Oxford University Computing Laboratory. {{cite journal}}:Cite 저널 요구 사항 journal=(도움말)
^ A.W. Roscoe (1994). "Model-checking CSP". In A Classical Mind: essays in Honour of C.A.R. Hoare. Prentice Hall. {{cite journal}}:Cite 저널 요구 사항 journal=(도움말)
^ "Introduction — FDR 4.2.4 documentation". www.cs.ox.ac.uk.
^ Parashkevov, Atanas N.; Yantchev, Jay (1996). "ARC – a tool for efficient refinement and equivalence checking for CSP". IEEE Int. Conf. on Algorithms and Architectures for Parallel Processing ICA3PP '96. pp. 68–75. CiteSeerX 10.1.1.45.3212.
^ Leuschel, Michael; Fontaine, Marc (2008). "Probing the Depths of CSP-M: A new FDR-compliant Validation Tool" (PDF). ICFEM 2008. Springer-Verlag. Archived from the original (PDF) on 2011-07-19. Retrieved 2008-11-26.
^ Sun, Jun; Liu, Yang; Dong, Jin Song (2009). "PAT: Towards Flexible Verification under Fairness" (PDF). Proceedings of the 20th International Conference on Computer-Aided Verification (CAV 2009). Lecture Notes in Computer Science. Vol. 5643. Springer. Archived from the original (PDF) on 2011-06-11. Retrieved 2009-06-16.
^ Sun, Jun; Liu, Yang; Dong, Jin Song (2008). "Model Checking CSP Revisited: Introducing a Process Analysis Toolkit" (PDF). Proceedings of the Third International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2008). Communications in Computer and Information Science. Vol. 17. Springer. pp. 307–322. Archived from the original (PDF) on 2009-01-08. Retrieved 2009-01-15.
^ Sun, Jun; Liu, Yang; Dong, Jin Song; Chen, Chunqing (2009). "Integrating Specifications and Programs for System Specification and Verification" (PDF). IEEE Int. Conf. on Theoretical Aspects of Software Engineering TASE '09. Archived from the original (PDF) on 2011-06-11. Retrieved 2009-04-13.
^ Green, Mark; Abdallah, Ali (2002). "Performance Analysis and Behaviour Tuning for Optimisation of Communicating Systems". Communicating Process Architectures 2002.
^ Brooke, Phillip; Paige, Richard (2007). "Lazy Exploration and Checking of CSP Models with CSPsim". Communicating Process Architectures 2007.
^ ISO 8807, 임시 주문 사양 언어
^ Geraint Jones (1990). "Sharp as a Razor: A Queen's Award for the Computing Laboratory". The Oxford Magazine (59, Fourth Week, Trinity Term).
^ Len Shustek (March 2009). "An interview with C.A.R. Hoare". Communications of the ACM. 52 (3): 38–41. doi:10.1145/1467247.1467261. S2CID 1868477.

추가 정보

Hoare, C. A. R. (2004) [1985]. Communicating Sequential Processes. Prentice Hall International. ISBN 978-0-13-153271-7.
- 이 책은 옥스퍼드 대학 컴퓨팅 연구소의 Jim Davies에 의해 갱신되었습니다.새로운 에디션은 Using CSP 웹사이트에서 PDF 파일로 다운로드 할 수 있습니다.
Roscoe, A. W. (1997). The Theory and Practice of Concurrency. Prentice Hall. ISBN 978-0-13-674409-2.
- 이 책과 관련된 링크는 여기에서 볼 수 있습니다.전문은 Bill Roscoe의 학술 출판물 목록에서 PS 또는 PDF 파일로 다운로드할 수 있습니다.

외부 링크

CSP의 주석(중국어판) 비영리 번역 및 주석 작업은 프렌티스홀 서적(1985년), 차오첸저우의 중국어판(1988년), 짐 데이비스의 온라인판(2015년)을 기반으로 한다.
CSP 및 occam 스타일 시스템용 사용자 그룹인 WoTUG에는 CSP 및 유용한 링크에 대한 몇 가지 정보가 포함되어 있습니다.
CiteSeer의 CSP 인용문

[roscoe-1] Roscoe, A. W. (1997). The Theory and Practice of Concurrency (PDF). Prentice Hall. ISBN 978-0-13-674409-2.

[2] Inmos (1995-05-12). occam 2.1 Reference Manual (PDF). SGS-THOMSON Microelectronics Ltd., INMOS 문서 72 oc 45 03.

[cox-3] Cox, Russ. "Bell Labs and CSP Threads". Retrieved 2010-04-15.

[4] "10 Academic and Historical Questions". Retrieved 2021-11-15.

[golang-5] "FAQ: Why build concurrency on the ideas of CSP?". The Go Programming Language. Retrieved 2021-10-15.

[clojure-core-async-6] Hickey, Rich (2013-06-28). "Clojure core.async Channels". Retrieved 2021-10-15.

[hoare1978-7] Hoare, C. A. R. (1978). "Communicating sequential processes". Communications of the ACM. 21 (8): 666–677. doi:10.1145/359576.359585. S2CID 849342.

[25years-8] Abdallah, Ali E.; Jones, Cliff B.; Sanders, Jeff W. (2005). Communicating Sequential Processes: The First 25 Years. LNCS. Vol. 3525. Springer. ISBN 9783540258131.

[barrett-9] Barrett, G. (1995). "Model checking in practice: The T9000 Virtual Channel Processor". IEEE Transactions on Software Engineering. 21 (2): 69–78. doi:10.1109/32.345823.

[hall-10] Hall, A; Chapman, R. (2002). "Correctness by construction: Developing a commercial secure system" (PDF). IEEE Software. 19 (1): 18–25. CiteSeerX 10.1.1.16.1811. doi:10.1109/52.976937.

[11] Creese, S. (2001). Data Independent Induction: CSP Model Checking of Arbitrary Sized Networks (D. Phil.). Oxford University. CiteSeerX 10.1.1.13.7185.

[hoare-12] Hoare, C. A. R. (1985). Communicating Sequential Processes. Prentice Hall. ISBN 978-0-13-153289-2.

[clinger1981-13] Clinger, William (June 1981). Foundations of Actor Semantics (Mathematics Doctoral Dissertation). MIT. hdl:1721.1/6935.

[14] Brookes, Stephen; Hoare, C. A. R.; Roscoe, A. W. (1984). "A Theory of Communicating Sequential Processes". Journal of the ACM. 31 (3): 560–599. doi:10.1145/828.833. S2CID 488666.

[15] Buth, B.; M. Kouvaras; J. Peleska; H. Shi (December 1997). "Deadlock analysis for a fault-tolerant system". Proceedings of the 6th International Conference on Algebraic Methodology and Software Technology (AMAST’97). pp. 60–75.

[16] Buth, B.; J. Peleska; H. Shi (January 1999). "Combining methods for the livelock analysis of a fault-tolerant system". Proceedings of the 7th International Conference on Algebraic Methodology and Software Technology (AMAST’98). pp. 124–139.

[17] Lowe, G. (1996). "Breaking and fixing the Needham–Schroeder public-key protocol using FDR". Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer-Verlag. pp. 147–166.

[18] Scattergood, J.B. (1998). "The Semantics and Implementation of Machine-Readable CSP". D.Phil. Oxford University Computing Laboratory. {{cite journal}}:Cite 저널 요구 사항 journal=(도움말)

[19] A.W. Roscoe (1994). "Model-checking CSP". In A Classical Mind: essays in Honour of C.A.R. Hoare. Prentice Hall. {{cite journal}}:Cite 저널 요구 사항 journal=(도움말)

[20] "Introduction — FDR 4.2.4 documentation". www.cs.ox.ac.uk.

[21] Parashkevov, Atanas N.; Yantchev, Jay (1996). "ARC – a tool for efficient refinement and equivalence checking for CSP". IEEE Int. Conf. on Algorithms and Architectures for Parallel Processing ICA3PP '96. pp. 68–75. CiteSeerX 10.1.1.45.3212.

[22] Leuschel, Michael; Fontaine, Marc (2008). "Probing the Depths of CSP-M: A new FDR-compliant Validation Tool" (PDF). ICFEM 2008. Springer-Verlag. Archived from the original (PDF) on 2011-07-19. Retrieved 2008-11-26.

[23] Sun, Jun; Liu, Yang; Dong, Jin Song (2009). "PAT: Towards Flexible Verification under Fairness" (PDF). Proceedings of the 20th International Conference on Computer-Aided Verification (CAV 2009). Lecture Notes in Computer Science. Vol. 5643. Springer. Archived from the original (PDF) on 2011-06-11. Retrieved 2009-06-16.

[24] Sun, Jun; Liu, Yang; Dong, Jin Song (2008). "Model Checking CSP Revisited: Introducing a Process Analysis Toolkit" (PDF). Proceedings of the Third International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2008). Communications in Computer and Information Science. Vol. 17. Springer. pp. 307–322. Archived from the original (PDF) on 2009-01-08. Retrieved 2009-01-15.

[25] Sun, Jun; Liu, Yang; Dong, Jin Song; Chen, Chunqing (2009). "Integrating Specifications and Programs for System Specification and Verification" (PDF). IEEE Int. Conf. on Theoretical Aspects of Software Engineering TASE '09. Archived from the original (PDF) on 2011-06-11. Retrieved 2009-04-13.

[26] Green, Mark; Abdallah, Ali (2002). "Performance Analysis and Behaviour Tuning for Optimisation of Communicating Systems". Communicating Process Architectures 2002.

[27] Brooke, Phillip; Paige, Richard (2007). "Lazy Exploration and Checking of CSP Models with CSPsim". Communicating Process Architectures 2007.

[28] ISO 8807, 임시 주문 사양 언어

[29] Geraint Jones (1990). "Sharp as a Razor: A Queen's Award for the Computing Laboratory". The Oxford Magazine (59, Fourth Week, Trinity Term).

[30] Len Shustek (March 2009). "An interview with C.A.R. Hoare". Communications of the ACM. 52 (3): 38–41. doi:10.1145/1467247.1467261. S2CID 1868477.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]

[19]

[20]

[21]

[22]

[25]

[26]

[27]

[28]

[29]

[30]

v t 동시 컴퓨팅
일반	동시성 동시성 제어 선형성
공정계산	CSP CCS ACP 로고 - - calculuscalculus 환경미적분 API 계산 PEPA 결합계산
고전적인 문제	ABA 문제 흡연자 문제 교착 상태 식사 철학자의 문제 생산자-소비자 레이스 조건 독자-라이터 문제 잠자는 이발사 문제
카테고리: 동시 컴퓨팅

Search

순차 프로세스 전달

네임스페이스

더

목차

역사

적용들

비공식적인 설명

원어민

대수 연산자

예

형식적 정의

구문

형식 의미론

표기 의미론

도구들

관련 형식

배우 모델과의 비교

상

「」를 참조해 주세요.

레퍼런스

추가 정보

외부 링크

Search

순차 프로세스 전달

역사

적용들

비공식적인 설명

원어민

대수 연산자

예

형식적 정의

구문

형식 의미론

표기 의미론

도구들

관련 형식

배우 모델과의 비교

상

「 」를 참조해 주세요.

레퍼런스

추가 정보

외부 링크

「」를 참조해 주세요.