커뮤니케이팅 시퀜셜 프로세스

"오늘의AI위키"는 AI 기술로 일관성 있고 체계적인 최신 지식을 제공하는 혁신 플랫폼입니다.
"오늘의AI위키"의 AI를 통해 더욱 풍부하고 폭넓은 지식 경험을 누리세요.

1. 개요
2. 역사
- 2.1. 원본 버전
- 2.2. 프로세스 대수로의 발전
3. 주요 개념
- 3.1. 기본 요소
- 3.2. 대수 연산자
4. 형식적 정의
- 4.1. 구문
- 4.2. 형식 의미론
5. 응용 분야
6. 관련 도구
7. 관련 형식론
8. 액터 모델과의 비교
9. 수상
참조

1. 개요

커뮤니케이팅 시퀜셜 프로세스(CSP)는 1978년 토니 호어에 의해 제시된 병렬 프로그래밍 언어이자 프로세스 대수이다. CSP는 병렬 프로세스 간의 통신 및 동기화를 모델링하며, 이벤트와 대수 연산자를 사용하여 시스템을 정의한다. CSP는 INMOS T9000 트랜스퓨터의 명세 및 검증, 소프트웨어 설계, 통신 및 보안 프로토콜 검증 등 다양한 분야에 응용되었으며, FDR과 같은 분석 도구를 통해 시스템의 정확성을 검증하는 데 활용된다. CSP는 액터 모델과 유사한 점이 있지만, 프로세스의 익명성, 명시적 채널 사용, 동기식 메시지 전달 등의 차이점을 보인다.

더 읽어볼만한 페이지

1978년 컴퓨팅 - SAP SE
SAP SE는 독일의 다국적 소프트웨어 기업으로, 전사적 자원 관리(ERP) 소프트웨어를 주력으로 다양한 소프트웨어 제품 및 서비스를 제공하며, 클라우드 기반 기술로의 전환과 사업 확장, 그리고 사회적 책임 관련 논란이 있다.
병행 컴퓨팅 - 슈퍼컴퓨터
슈퍼컴퓨터는 일반 컴퓨터보다 훨씬 높은 성능을 가진 컴퓨터로, 복잡한 계산과 시뮬레이션을 수행하며, 프로세서, 메모리, 스토리지, 네트워크 등으로 구성되어 병렬 처리를 통해 높은 성능을 구현하고, 군사, 기상 예측, 과학 기술 분야, 인공지능 등 다양한 분야에서 활용되고 있다.
병행 컴퓨팅 - 프로세스
프로세스는 컴퓨터에서 실행되는 프로그램의 인스턴스로, 운영 체제가 시스템 자원을 효율적으로 관리하며 멀티태스킹 환경에서 독립적인 실행 흐름을 유지한다.

커뮤니케이팅 시퀜셜 프로세스
개요
이름	커뮤니케이팅 시퀀셜 프로세스
로마자 표기	Keomyunikeiting Sikeonsyeol Peuroseseu
약자	CSP
종류	형식 검증 언어
패러다임	병행성
설계자
개발자	토니 호어
영향
영향을 준 언어	오컴 에르랑 림보 Go 코어.async JCSP
특징
주요 특징	프로세스 간의 통신을 위한 채널 기반 통신 결정론적이고 수학적으로 엄격한 의미론 병행 시스템의 모델링 및 검증에 적합
사용 분야	병행 시스템 설계 및 검증 프로토콜 검증 분산 시스템 모델링
참고 문헌
관련 서적	Communicating Sequential Processes: The First 25 Years The Theory and Practice of Concurrency
기타
관련 링크	Bell Labs and CSP Threads 10 Academic and Historical Questions FAQ: Why build concurrency on the ideas of CSP? Clojure core.async Channels

2. 역사

CSP는 1978년 토니 호어의 논문에서 처음 제시되었다. 초기 버전은 프로세스 대수보다는 병렬 프로그래밍 언어에 가까웠으며, 이후 버전들과는 구문이 다르고 수학적으로 정의된 의미론을 갖지 않았다.^[38] 또한 제한 없는 비결정성을 표현할 수 없었다.^[39]

그 후 호어는 스티븐 브룩스(Stephen Brookes), 빌 로스코(Bill Roscoe) 등과 함께 이론적인 면을 개선하여 CSP를 프로세스 대수적으로 발전시켰다. 이는 동시기에 로빈 밀너가 진행했던 계산적 통신 시스템(CCS) 연구와 상호 영향을 주고받았다. CSP의 이론적인 면은 1984년에 발표되었고,^[40] 1985년에 출판된 호어의 저서 ''Communicating Sequential Processes''^[38]에서 널리 알려졌다. 2006년 9월 현재에도 Citeseer에 따르면 이 책은 컴퓨터 과학 분야에서 [http://citeseer.ist.psu.edu/articles.html 인용 횟수 3위]로 되어 있으나, 샘플링 방식이므로 신뢰도는 높지 않다. 호어의 저서 이후 CSP 이론은 약간 변경되었을 뿐이며, 변경의 대부분은 CSP 프로세스 분석 및 검증을 위한 자동화 도구의 출현에 대응하는 것이다. 로스코의 ''The Theory and Practice of Concurrency''^[32]에서는 이 새로운 CSP가 해설되어 있다.

2. 1. 원본 버전

1978년 토니 호어의 원본 논문에 제시된 CSP 버전은 프로세스 대수가 아닌 본질적으로 동시 프로그래밍 언어였다. 이는 이후 버전의 CSP와는 상당히 다른 구문을 가지고 있었으며, 수학적으로 정의된 의미론을 갖지 않았고,^[12] 무한 비결정성을 표현할 수 없었다.^[13] 원래 CSP의 프로그램은 고정된 수의 순차적 프로세스들이 동기식 메시지 전달을 통해 서로 통신하는 병렬 구성으로 작성되었다. 이후 버전의 CSP와는 대조적으로, 각 프로세스에는 명시적인 이름이 할당되었고, 메시지의 송신자 또는 수신자는 의도된 송신 또는 수신 프로세스의 이름을 지정하여 정의되었다. 예를 들어, 다음 프로세스와 같다.

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

이 프로세스는 `west`라는 프로세스에서 문자를 반복적으로 수신하여 `east`라는 프로세스로 해당 문자를 전송한다. 병렬 구성은 다음과 같다.

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

이것은 `west`를 `DISASSEMBLE` 프로세스에, `X`를 `COPY` 프로세스에, 그리고 `east`를 `ASSEMBLE` 프로세스에 할당하고, 이 세 프로세스를 동시에 실행한다.^[7]

2. 2. 프로세스 대수로의 발전

커뮤니케이팅 시퀜셜 프로세스(CSP)의 원본 버전 출판 이후, 호어, 스티븐 브룩스, A. W. 로스코는 CSP의 ''이론''을 현대적인 프로세스 대수 형태로 발전시키고 다듬었다. CSP를 프로세스 대수로 발전시키는 데 사용된 접근 방식은 로빈 밀너의 계산적 통신 시스템(CCS) 연구에 영향을 받았으며, 그 반대의 경우도 마찬가지였다.^[14] CSP의 이론적 버전은 브룩스, 호어, 로스코의 1984년 논문과 1985년에 출판된 호어의 저서 ''통신 순차 프로세스''(Communicating Sequential Processes)에 처음 소개되었다.^[12] 2006년 9월, 해당 도서는 CiteSeer에 따르면 (샘플링 특성상 신뢰할 수 없는 출처이지만) 여전히 세 번째로 많이 인용된 컴퓨터 과학 참고 자료였다. CSP 이론은 호어의 저서 출판 이후 몇 가지 사소한 변화를 겪었다. 이러한 변화의 대부분은 CSP 프로세스 분석 및 검증을 위한 자동화 도구의 출현에 의해 동기 부여되었다. 로스코의 ''병행성의 이론과 실제''는 이러한 새로운 버전의 CSP를 설명한다.^[1]

3. 주요 개념

CSP는 독립적으로 작동하고 오직 메시지 전달 통신을 통해서만 서로 상호 작용하는 구성 요소 프로세스 측면에서 시스템을 설명할 수 있게 해준다. 현대 CSP는 구성 요소 프로세스를 순차적 프로세스뿐만 아니라 더 기본적인 프로세스의 병렬 구성으로도 정의할 수 있기 때문에, CSP 이름의 '순차적(Sequential)' 부분은 다소 부적절한 표현이다.^[18]

다양한 프로세스 대수 연산자를 사용하여 서로 다른 프로세스 간의 관계와 각 프로세스가 해당 환경과 통신하는 방식을 설명한다. 이 대수적 접근 방식을 사용하면 몇 가지 기본 요소만으로 매우 복잡한 프로세스 설명을 쉽게 구성할 수 있다.^[18]

3. 1. 기본 요소

CSP는 프로세스 대수에서 두 종류의 기본 요소, 즉 이벤트와 기본 프로세스를 제공한다.^[18]

; 이벤트

: 이벤트는 통신 또는 상호 작용을 의미한다. 분할 불가능하고 순간적인 것으로 간주된다. 원자 이름(예:

\mathit{on}

,

\mathit{off}

), 복합 이름(예:

valve.open

,

valve.close

), 또는 입력/출력 이벤트(예:

mouse?xy

,

screen!bitmap

)일 수 있다. 모든 이벤트 집합은

\Sigma

로 표시된다.

; 기본 프로세스

: 기본 프로세스는 기본적인 동작을 나타낸다. 예시로는

\mathrm{STOP}

(즉시 데드락되는 프로세스)와

\mathrm{SKIP}

(즉시 성공적으로 종료되는 프로세스)가 있다.

3. 2. 대수 연산자

CSP는 다양한 대수 연산자를 사용하여 프로세스 간의 관계 및 통신 방식을 정의한다. 주요 연산자는 다음과 같다.

프리픽스 (Prefix): 프리픽스 연산자는 이벤트와 프로세스를 결합하여 새로운 프로세스를 만든다. 예를 들어, $a \rightarrow P$ 는 환경과 이벤트 $a$ 를 통신하려는 프로세스이며, $a$ 이후에는 프로세스 $P$ 처럼 동작한다.

결정적 선택 (Deterministic Choice): 결정적 (또는 외부) 선택 연산자는 프로세스의 향후 진화를 두 개의 구성 요소 프로세스 간의 선택으로 정의할 수 있게 하며, 환경이 프로세스 중 하나의 초기 이벤트를 통신하여 선택을 해결할 수 있게 한다. 예를 들어, $(a \rightarrow P) \Box (b \rightarrow Q)$ 는 초기 이벤트 $a$ 와 $b$ 를 통신하려는 프로세스이며, 환경이 어떤 초기 이벤트를 통신하는지에 따라 $P$ 또는 $Q$ 로 동작한다.

비결정적 선택 (Nondeterministic Choice): 비결정적 (또는 내부) 선택 연산자는 프로세스의 향후 진화를 두 개의 구성 요소 프로세스 간의 선택으로 정의할 수 있게 하지만, 환경이 구성 요소 프로세스 중 어떤 프로세스가 선택될지 제어할 수 없게 한다. 예를 들어, $(a \rightarrow P) \sqcap (b \rightarrow Q)$ 는 $a \rightarrow P$ 또는 $b \rightarrow Q$ 처럼 동작할 수 있다. $a$ 또는 $b$ 의 수신을 거부할 수 있으며, 환경이 $a$ 와 $b$ 를 모두 제공하는 경우에만 통신할 의무가 있다. 선택의 양쪽 측면의 초기 이벤트가 동일한 경우, 명목상 결정적 선택에 의도하지 않게 비결정성이 도입될 수 있다. 예를 들어 $(a \rightarrow a \rightarrow \mathrm{STOP}) \Box (a \rightarrow b \rightarrow \mathrm{STOP})$ 와 $a \rightarrow ((a \rightarrow \mathrm{STOP}) \sqcap (b \rightarrow \mathrm{STOP}))$ 는 동일하다.

인터리빙 (Interleaving): 인터리빙 연산자는 완전히 독립적인 동시 활동을 나타낸다. 프로세스 $P \;|||\; Q$ 는 $P$ 와 $Q$ 모두와 동시에 동작한다. 두 프로세스의 이벤트는 임의의 시간 순서로 인터리빙된다.

인터페이스 병렬 (Interface Parallel): 인터페이스 병렬 (또는 일반화된 병렬) 연산자는 구성 요소 프로세스 간의 동기화가 필요한 동시 활동을 나타낸다. $P \;|[X]|\; Q$ 의 경우, 인터페이스 집합 $X \subseteq \Sigma$ 의 모든 이벤트는 $P$ 와 $Q$ 가 모두 해당 이벤트에 참여할 수 있을 때만 발생할 수 있다. 예를 들어, 프로세스 $P \;|[\{ a \}]|\; Q$ 는 $P$ 와 $Q$ 가 모두 이벤트 $a$ 를 수행할 수 있어야 해당 이벤트가 발생할 수 있다. 따라서, 프로세스 $(a \to P) \;|[\{ a \}]|\; (a \to Q)$ 는 $a \to (P \;|[\{ a \}]|\; Q)$ 와 동일하고, $(a \to P ) \;|[\{ a, b \}]|\; (b \to Q)$ 는 $\mathrm{STOP}$ (즉, 프로세스 데드락)과 동일하다.

숨기기 (Hiding): 숨기기 연산자는 환경에서 일부 이벤트를 관찰할 수 없도록 하여 프로세스를 추상화하는 방법을 제공한다. $P \setminus X$ 는 이벤트 집합 $X$ 가 숨겨진 프로세스 $P$ 이다.

4. 형식적 정의

CSP의 형식 의미론은 구문적으로 올바른 표현식에 "의미"를 부여하기 위해 사용된다. CSP 이론은 지시적 의미론, 대수적 의미론, 운영 의미론을 포함한 여러 의미론적 접근 방식을 제공한다.^[1]

CSP의 세 가지 주요 지시적 의미론 모델은 다음과 같다.

추적 모델 (Traces Model): 프로세스가 수행할 수 있는 이벤트의 시퀀스(추적) 집합으로 프로세스의 의미를 정의한다. 예를 들어,
$\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^영어를 수행하는 것으로 관찰될 수 있다.

안정적 실패 모델 (Stable Failures Model): 추적 모델을 확장하여 거부 집합(프로세스가 수행을 거부할 수 있는 이벤트 집합)을 포함한다. '실패'는 추적 s^영어와 거부 집합 X^영어의 쌍 $\left(s,X\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\}$

실패/발산 모델 (Failures/Divergence Model): 실패 모델을 더욱 확장하여 발산(프로세스가 무한히 내부적인 동작을 수행하는 것)을 처리한다. 이 모델에서 프로세스의 의미는 $\left(\mathrm{failures}_\perp\left(P\right), \mathrm{divergences}\left(P\right)\right)$ 쌍으로 표현된다.

4. 1. 구문

CSP의 구문은 프로세스와 이벤트를 결합할 수 있는 "합법적인" 방식을 정의한다. ''e''를 이벤트, ''X''를 이벤트 집합이라고 하자. 그러면 CSP의 기본 구문은 다음과 같이 정의할 수 있다.

:

\begin{array}{lcll}{Proc} & ::= & \mathrm{STOP} & \; \\&|& \mathrm{SKIP} & \; \\&|& 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{병렬})\\&|& {Proc} \setminus X & (\text{숨기기})\\&|& {Proc} \; ; {Proc} & (\text{순차적} \; \text{구성})\\&|& \mathrm{if} \; b \; \mathrm{then} \; {Proc}\; \mathrm{else}\; Proc & (\text{불리언} \; \text{조건})\\&|& {Proc} \;\triangleright\; {Proc} & (\text{타임 아웃})\\&|& {Proc} \;\triangle\; {Proc} & (\text{인터럽트})\end{array}

위에 제시된 구문은 간결성을 위해 다이버전스를 나타내는

\mathbf{div}

프로세스와 정렬된 병렬, 파이핑, 인덱스 선택과 같은 다양한 연산자를 생략한다.

4. 2. 형식 의미론

CSP는 구문적으로 올바른 표현식의 "의미"를 정의하기 위해 여러 가지 형식 의미론을 부여받았다.^[1] CSP 이론은 상호 일관된 지시적 의미론, 대수적 의미론, 운영 의미론을 포함한다.

CSP의 세 가지 주요 지시적 의미론 모델은 '추적' 모델, '안정적 실패' 모델, '실패/발산' 모델이다. 프로세스 표현식에서 이 세 모델 각각에 대한 의미 매핑은 CSP에 대한 지시적 의미론을 제공한다.^[1]

추적 모델은 프로세스 표현식의 의미를 프로세스가 수행할 수 있다고 관찰되는 이벤트 시퀀스(추적)의 집합으로 정의한다. 예를 들면 다음과 같다.

$\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$ 이다. '실패'는 추적 s^영어와 프로세스가 추적 s^영어를 실행한 후 거부할 수 있는 이벤트를 식별하는 거부 집합 X^영어로 구성된 쌍 $\left(s,X\right)$ 이다. 안정적 실패 모델에서 프로세스의 관찰된 동작은 쌍 $\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\}$ 이다.

5. 응용 분야

CSP는 시스템 모델링, 분석 및 검증 등 다양한 분야에 응용된다.

CSP는 초기에 INMOS T9000 트랜스퓨터의 사양 기술 및 검증에 사용되었다.^[35] T9000은 복잡한 슈퍼스칼라형 파이프라인 프로세서로, 대규모 멀티프로세싱을 지원하도록 설계되었다. CSP는 파이프라인과 칩 간 통신 관리 기능(Virtual Channel Processor)의 정당성을 검증하는 데 사용되었다.

소프트웨어 설계에서 CSP는 주로 인명과 관련된 중요한 시스템에 응용된다. 브레멘 안전 시스템 연구소와 다임러-벤츠 에어로스페이스는 국제 우주 정거장 시스템(약 23,000행 코드)을 CSP로 모델링하여 데드락 및 라이브락 발생 여부를 검증했다.^[42]^[43] 이를 통해 일반적인 소프트웨어 테스트로는 발견하기 어려운 문제를 찾아낼 수 있었다. 프락시스 হাই 인테그리티 시스템즈(Praxis High Integrity Systems)는 보안 스마트 카드 인증 시스템(약 100,000행 코드) 개발에 CSP를 사용하여 보안 및 데드락 문제를 검증했으며, 그 결과 시스템 결함률이 낮아졌다고 주장한다.^[36]

CSP는 메시지 교환을 사용하는 복잡한 시스템 모델링 및 분석에 적합하여 통신 및 보안 프로토콜 검증에도 활용된다. 특히 니덤-슈뢰더 공개 키 인증 프로토콜 검증에 CSP를 사용하여 알려지지 않은 취약점을 발견하고, 이를 보완한 새로운 프로토콜을 개발한 사례가 주목할 만하다.^[44]

5. 1. 하드웨어 설계

CSP의 초기이자 중요한 응용 분야는 대규모 다중 처리를 지원하도록 설계된 복잡한 슈퍼 스칼라 파이프라인 프로세서인 INMOS T9000 트랜스퓨터 요소의 명세 및 검증이었다. CSP는 프로세서 파이프라인과 프로세서의 칩 외부 통신을 관리하는 가상 채널 프로세서의 정확성을 검증하는 데 사용되었다.^[9]

5. 2. 소프트웨어 설계

CSP의 소프트웨어 설계에 대한 산업적 응용은 주로 신뢰성과 안전이 중요한 시스템에 집중되어 왔다. 예를 들어, 브레멘 안전 시스템 연구소와 다임러-벤츠 항공우주는 국제 우주 정거장에서 사용될 고장 관리 시스템 및 항공 전자 인터페이스(약 23,000줄의 코드)를 CSP로 모델링하고 분석하여, 설계에 데드락 및 라이브락이 없음을 확인했다.^[15]^[16] 이 모델링 및 분석 과정에서 테스트만으로는 발견하기 어려웠던 많은 오류들이 발견되었다.

마찬가지로, 프락시스 하이 인테그리티 시스템즈는 안전한 스마트 카드 인증 기관용 소프트웨어(약 100,000줄의 코드) 개발에 CSP 모델링 및 분석을 적용하여 설계의 안전성과 데드락 부재를 검증했다. 프락시스는 이 시스템의 결함률이 유사 시스템보다 훨씬 낮다고 주장한다.^[10]

CSP는 복잡한 메시지 교환을 포함하는 시스템을 모델링하고 분석하는 데 적합하여, 통신 및 보안 프로토콜 검증에도 활용되었다. 대표적인 예로, 로우는 CSP와 FDR 정제 검사기를 사용하여 니덤-슈뢰더 공개 키 인증 프로토콜에 대한 이전에는 알려지지 않았던 공격을 발견하고, 이를 방어할 수 있는 수정된 프로토콜을 개발했다.^[17]

5. 3. 프로토콜 검증

CSP는 통신 및 보안 프로토콜 검증에도 적용되었다. 특히, 로우는 CSP와 FDR 정제 검사기를 사용하여 니덤-슈뢰더 공개 키 인증 프로토콜에서 이전에 알려지지 않았던 공격을 발견하고, 이를 막을 수 있는 수정된 프로토콜을 개발하였다.^[17]

6. 관련 도구

CSP 모델링, 분석 및 검증을 위해 다양한 도구들이 개발되었다. 초기에는 도구마다 다른 기계 판독 가능 구문을 사용하여 호환성이 떨어졌다. 그러나 현재는 대부분 Bryan Scattergood가 고안한 CSP의 기계 판독 가능 방언인 CSP_''M''으로 표준화되었다.^[19] CSP_''M''은 공식적으로 정의된 동작적 의미론을 가지며, 내장된 함수형 프로그래밍 언어를 포함한다.

가장 잘 알려진 CSP 도구는 FDR (Failures-Divergences Refinement)이다. FDR은 원래 Formal Systems (Europe) Ltd.에서 개발한 상용 제품으로, 모델 검사기로 묘사되지만 기술적으로는 ''정제'' 검사기이다. FDR은 두 개의 CSP 프로세스 표현식을 레이블 전이 시스템(LTS)으로 변환한 다음, 지정된 의미 모델(추적, 실패 또는 실패/발산) 내에서 한 프로세스가 다른 프로세스의 정제인지 여부를 결정한다.^[20] 또한, 정제 검사 중 탐색해야 하는 상태 공간 크기를 줄이기 위해 프로세스 LTS에 다양한 상태 공간 압축 알고리즘을 적용한다. FDR의 후속 제품으로는 FDR2, FDR3, FDR4가 있다.^[21]

다른 주요 도구들은 다음과 같다:

애들레이드 정제 검사기(ARC):^[22] 애들레이드 대학교 형식 모델링 및 검증 그룹에서 개발한 CSP 정제 검사기이다. ARC는 내부적으로 CSP 프로세스를 정렬된 이진 결정 다이어그램(OBDD)으로 표현하여 FDR2와 차별화된다. 이는 FDR2에서 사용되는 상태 공간 압축 알고리즘 없이도 명시적 LTS 표현의 상태 폭발 문제를 완화한다.
ProB:^[23] 하인리히-하이네 뒤셀도르프 대학교 정보학 연구소에서 주최하며, B 방법으로 작성된 명세 분석을 지원하기 위해 만들어졌다. 그러나 정제 검사 및 LTL 모델 검사를 통한 CSP 프로세스 분석도 지원한다. ProB는 CSP와 B 명세를 결합한 속성 검증에도 사용될 수 있다. ProBE CSP 애니메이터는 FDR3에 통합되었다.
프로세스 분석 툴킷(PAT):^[24]^[25] 싱가포르 국립 대학교 전산학부에서 개발한 CSP 분석 도구이다. PAT는 CSP 및 시간적 CSP 프로세스의 정제 검사, LTL 모델 검사, 시뮬레이션을 수행할 수 있다. PAT 프로세스 언어는 CSP를 확장하여 가변 공유 변수, 비동기 메시지 전달, 다양한 공정성 및 정량적 시간 관련 프로세스 구성 요소(deadline, waituntil 등)를 지원한다. PAT 프로세스 언어는 표현력 확대를 위해 높은 수준의 사양 언어와 절차적 프로그램(예: PAT 이벤트는 순차 프로그램 또는 외부 C# 라이브러리 호출)을 결합한다. 가변 공유 변수와 비동기 채널은 표준 CSP에서 사용되는 프로세스 모델링 패턴에 대한 구문 설탕을 제공한다. PAT 구문은 CSP_''M''과 유사하지만, 프로세스 표현식 종료에 세미콜론을 사용하고 변수 및 할당에 대한 구문 설탕을 포함하며 내부 선택 및 병렬 구성에 약간 다른 구문을 사용한다는 점에서 차이가 있다.^[26]
VisualNets:^[27] 명세로부터 CSP 시스템의 애니메이션 시각화를 생성하며, 시간 CSP를 지원한다.
CSPsim:^[28] 느긋한 시뮬레이터로, CSP 모델 검사는 수행하지 않지만 매우 큰 (잠재적으로 무한한) 시스템 탐색에 유용하다.
[http://www.principia-m.com/syncstitch/ SyncStitch]: 대화형 모델링 및 분석 환경을 갖춘 CSP 정제 검사기이다. 그래픽 상태 전이 다이어그램 편집기를 통해 사용자는 CSP 표현식뿐만 아니라 상태 전이 다이어그램으로도 프로세스 동작을 모델링할 수 있다. 검사 결과는 계산 트리로 그래픽으로 보고되며, 주변 검사 도구와 함께 대화식으로 분석할 수 있다. 정제 검사 외에도 교착 상태 검사 및 활성 루프 검사도 가능하다.

7. 관련 형식론

다음은 CSP에서 파생되거나 영감을 받은 다양한 명세 언어 및 형식론이다.

http://citeseer.comp.nus.edu.sg/61363.html Timed CSP: 실시간 시스템에 대한 추론을 위해 타이밍 정보를 통합한다.
https://dx.doi.org/10.1007/BF01178564 수용적 프로세스 이론: 비동기식(논블로킹) 전송 연산을 가정하는 CSP의 특수화이다.
https://web.archive.org/web/20110514085953/http://www.wotug.org/paperdb/show_pap.php?f=1&num=394 CSPP
https://web.archive.org/web/20110514085958/http://www.wotug.org/paperdb/show_pap.php?f=1&num=395 HCSP
https://web.archive.org/web/20110514234220/http://www.comp.nus.edu.sg/~dongjs/tcoz.html TCOZ: Timed CSP와 Object Z의 통합이다.
https://web.archive.org/web/20110514234221/http://www.cs.york.ac.uk/circus/ Circus: Unifying Theories of Programming을 기반으로 한 CSP와 Z의 통합이다.
http://www.compass-research.eu/approach.html CML (COMPASS 모델링 언어): 시스템 오브 시스템 (SoS) 모델링을 위해 개발된 https://web.archive.org/web/20110514234221/http://www.cs.york.ac.uk/circus/ Circus와 VDM의 조합이다.
https://web.archive.org/web/20110514234221/http://www.cs.swan.ac.uk/~csmarkus/Papers/cspcasl.ps CspCASL: CSP를 통합하는 CASL의 확장이다.
LOTOS: CSP와 CCS의 기능을 통합한 국제 표준^[29]이다.
https://link.springer.com/chapter/10.1007/978-3-319-05032-4_25 PALPS: Anna Philippou와 Mauricio Toro Bermúdez가 개발한 생태 모델을 위한 위치가 있는 확률적 확장이다.

8. 액터 모델과의 비교

액터 모델은 메시지를 교환하는 병렬 프로세스와 관련하여 커뮤니케이팅 시퀜셜 프로세스(CSP)와 광범위하게 유사하다. 그러나 두 모델은 제공하는 기본 요소와 관련하여 근본적으로 다른 선택을 한다.

CSP 프로세스는 익명인 반면, 액터는 정체성을 갖는다.
CSP는 메시지 전달에 명시적 채널을 사용하는 반면, 액터 시스템은 명명된 대상 액터로 메시지를 전송한다. 이러한 접근 방식은 서로의 이중성으로 간주될 수 있다. 즉, 단일 채널을 통해 수신하는 프로세스는 해당 채널에 해당하는 정체성을 효과적으로 가지는 반면, 액터 간의 이름 기반 결합은 채널처럼 작동하는 액터를 구성하여 끊을 수 있다.
CSP 메시지 전달은 기본적으로 메시지 송수신에 관여하는 프로세스 간의 랑데부(rendezvous)를 포함한다. 즉, 수신자가 메시지를 수락할 준비가 될 때까지 발신자는 메시지를 전송할 수 없다. 반대로, 액터 시스템의 메시지 전달은 근본적으로 비동기식이다. 즉, 메시지 전송과 수신이 동시에 일어날 필요가 없으며, 발신자는 수신자가 메시지를 수락할 준비가 되기 전에 메시지를 전송할 수 있다. 이러한 접근 방식은 서로의 이중성으로 간주될 수도 있다. 즉, 랑데부 기반 시스템은 비동기 메시징 시스템처럼 작동하는 버퍼링된 통신을 구성하는 데 사용될 수 있는 반면, 비동기 시스템은 송신자와 수신자를 동기화하기 위해 메시지/응답 프로토콜을 사용하여 랑데부 스타일의 통신을 구성하는 데 사용될 수 있다.

위에서 언급한 속성은 호어(Hoare)의 원본 CSP 논문이 아니라, Go 및 Clojure의 core.async와 같은 구현에서 볼 수 있는 아이디어의 현대적 구현을 의미한다. 원본 논문에서 채널은 사양의 중심 부분이 아니었으며, 발신자와 수신 프로세스는 실제로 서로를 이름으로 식별했다.

9. 수상

1990년, 여왕 기술 혁신상이 옥스퍼드 대학교 컴퓨팅 연구소에 수여되었다. 이 상은 연구소와 인모스사 간의 성공적인 협력을 인정한 것이다.^[30] 인모스의 주력 제품은 '트랜스퓨터'였는데, 이는 일반적으로 추가로 필요한 여러 부품을 동일한 단일 부품에 내장한 마이크로프로세서였다.^[30]

토니 호어에 따르면, 인모스 트랜스퓨터는 서로 통신할 수 있는 마이크로프로세서를 구축하려는 아이디어를 구현한 것이었다.^[31] 창립자는 CSP 아이디어가 산업적으로 활용될 준비가 되었다는 비전을 가지고 있었고, 이를 트랜스퓨터 프로그래밍 언어( 오컴)의 기반으로 삼았다.^[31] 회사는 이를 통해 1년 더 빨리 하드웨어를 제공할 수 있었다고 추정했으며, 옥스퍼드 대학교 컴퓨팅 연구소와 협력하여 여왕 기술 혁신상을 신청하고 수상했다.^[31]

참조

_[1] 서적 The Theory and Practice of Concurrency http://www.cs.ox.ac.[...] Prentice Hall 1997
_[2] 서적 occam 2.1 Reference Manual http://www.wotug.org[...] SGS-Thomson Microelectronics Ltd. 1995-05-12
_[3] 웹사이트 Bell Labs and CSP Threads http://swtch.com/~rs[...] 2010-04-15
_[4] 웹사이트 10 Academic and Historical Questions https://www.erlang.o[...] 2021-11-15
_[5] 웹사이트 FAQ: Why build concurrency on the ideas of CSP? http://golang.org/do[...] 2021-10-15
_[6] 웹사이트 Clojure core.async Channels https://clojure.org/[...] 2013-06-28
_[7] 간행물 Communicating sequential processes 1978
_[8] 서적 Communicating Sequential Processes: The First 25 Years https://www.springer[...] Springer 2005
_[9] 간행물 Model checking in practice: The T9000 Virtual Channel Processor 1995
_[10] 간행물 Correctness by construction: Developing a commercial secure system http://www.anthonyha[...] 2002
_[11] 학위논문 Data Independent Induction: CSP Model Checking of Arbitrary Sized Networks Oxford University 2001
_[12] 서적 Communicating Sequential Processes Prentice Hall 1985
_[13] Mathematics Doctoral Dissertation Foundations of Actor Semantics MIT 1981-06
_[14] 간행물 A Theory of Communicating Sequential Processes 1984
_[15] 학술회의 Deadlock analysis for a fault-tolerant system 1997-12
_[16] 학술회의 Combining methods for the livelock analysis of a fault-tolerant system 1999-01
_[17] 학술회의 Breaking and fixing the Needham–Schroeder public-key protocol using FDR http://citeseer.ist.[...] Springer-Verlag 1996
_[18] 서적 Understanding Concurrent Systems 2010
_[19] 학위논문 The Semantics and Implementation of Machine-Readable CSP Oxford University Computing Laboratory 1998
_[20] 서적 A Classical Mind: Essays in Honour of C. A. R. Hoare Prentice Hall 1994
_[21] 웹사이트 Introduction — FDR 4.2.4 documentation https://www.cs.ox.ac[...]
_[22] 학술회의 ARC – a tool for efficient refinement and equivalence checking for CSP 1996
_[23] 학술회의 Probing the Depths of CSP-M: A new FDR-compliant Validation Tool http://www.stups.uni[...] Springer-Verlag 2008-11-26
_[24] 학술회의 PAT: Towards Flexible Verification under Fairness http://www.comp.nus.[...] Springer 2009-06-16
_[25] 학술회의 Model Checking CSP Revisited: Introducing a Process Analysis Toolkit http://www.comp.nus.[...] Springer 2009-01-15
_[26] 학술회의 Integrating Specifications and Programs for System Specification and Verification http://www.comp.nus.[...] 2009-04-13
_[27] 학술회의 Performance Analysis and Behaviour Tuning for Optimisation of Communicating Systems https://www.research[...] 2002
_[28] 학술회의 Lazy Exploration and Checking of CSP Models with CSPsim 2007
_[29] 문서 ISO 8807, Language of Temporal Ordering Specification
_[30] 간행물 Sharp as a Razor: A Queen's Award for the Computing Laboratory http://www.cs.ox.ac.[...] 1990
_[31] 간행물 An interview with C.A.R. Hoare https://dl.acm.org/d[...] 2009-03
_[32] 서적 The Theory and Practice of Concurrency Prentice Hall 1997
_[33] 서적 occam 2.1 Reference Manual http://www.wotug.org[...] SGS-THOMSON Microelectronics Ltd. 1995-05-12
_[34] 간행물 Communicating sequential processes 1978
_[35] 간행물 Model checking in practice: The T9000 Virtual Channel Processor 1995
_[36] 간행물 Correctness by construction: Developing a commercial secure system http://www.anthonyha[...] 2002-01-01
_[37] 논문 Data Independent Induction: CSP Model Checking of Arbitrary Sized Networks Oxford University 2001-01-01
_[38] 서적 Communicating Sequential Processes Prentice Hall
_[39] 논문 Foundations of Actor Semantics https://dspace.mit.e[...] MIT 1981-06-01
_[40] 간행물 A Theory of Communicating Sequential Processes 1984-01-01
_[41] 문서 計算機科学では、計算が終了しないか、例外的な状態で終了する場合、その計算は発散すると言われる、そうでない場合は収束すると言われる。プロセス計算など、計算が無限に続くことが予想される領域では、計算が生産的でない場合（すなわち、有限の時間内に行動を生み出し続けることができない場合）に、計算が発散すると言われる。
_[42] 학회자료 Deadlock analysis for a fault-tolerant system 1997-12-01
_[43] 학회자료 Combining methods for the livelock analysis of a fault-tolerant system 1999-01-01
_[44] 학회자료 Breaking and fixing the Needham-Schroeder public-key protocol using FDR http://citeseer.ist.[...] Springer-Verlag 1996-01-01
_[45] 논문 The Semantics and Implementation of Machine-Readable CSP Oxford University Computing Laboratory 1998-01-01
_[46] 논문 Model-checking CSP Prentice Hall 1994-01-01
_[47] 웹인용 "FAQ: Why build concurrency on the ideas of CSP?" https://go.dev/doc/f[...] 2023-05-04

본 사이트는 AI가 위키백과와 뉴스 기사,정부 간행물,학술 논문등을 바탕으로 정보를 가공하여 제공하는 백과사전형 서비스입니다.
모든 문서는 AI에 의해 자동 생성되며, CC BY-SA 4.0 라이선스에 따라 이용할 수 있습니다.
하지만, 위키백과나 뉴스 기사 자체에 오류, 부정확한 정보, 또는 가짜 뉴스가 포함될 수 있으며, AI는 이러한 내용을 완벽하게 걸러내지 못할 수 있습니다.
따라서 제공되는 정보에 일부 오류나 편향이 있을 수 있으므로, 중요한 정보는 반드시 다른 출처를 통해 교차 검증하시기 바랍니다.

문의하기 : help@durumis.com