什么是CSP介绍

Communication Sequential Process （简称CSP）是著名计算机科学家托尼·霍尔为解决并发现象而提出的代数理论，是一个专为描述并发系统中通过消息交换进行交互通信实体行为而设计的一种抽象语言。

CSP简介

可用FDR（Failure Divergence Refinement）验证设计是否正确。

在该语言中，一个并发系统由若干并行运行的顺序进程组成，每个进程不能对其他进程的变量赋值。进程之间只能通过 一对通信原语实现协作：Q->x表示从进程Q输入一个值到变量x中；Px， 同时Q进程执行P<-e时，发生通信，e的值从Q进程传送给P进程的变量x。后来出现的实用编程语言OCCAM即以CSP为基础发展而成。

1984年S．Brooks，托尼·霍尔和W．Roscoe提出CSP理论(TCSP)。这是一个代数演算系统，其基本成分是事件(或动 作)。进程由事件和一组算子构造而成。

典型的算子有：→(前缀)，|(外部非确定性选择)，e(事件隐蔽)，以及递归等。

CSP例子

例：(自动售货机) VM=coin→(choc→VM|coffee→VM)， CUST：coin→(choc→CUST coffee→CUST) 这里定义了两个进程：VM(售货机)和CUST (顾客)。售货机在接受了硬币coin后，可按顾客的要求支付choc或coffee。顾客在付了硬币后，或者想要choc，或者想要coffee，其选 择不受外界影响。