-
CSP
(通信順序進程)
鎖定
Communication Sequential Process (簡稱CSP)是著名計算機科學家託尼·霍爾為解決並發現象而提出的代數理論,是一個專為描述併發系統中通過消息交換進行交互通信實體行為而設計的一種抽象語言。
[1]
- 外文名
- CSP
- 創始人
- 託尼·霍爾
- 類 別
- 代數理論
- 應 用
- 交互通信實體行為
CSP簡介
可用FDR(Failure Divergence Refinement)驗證設計是否正確。
在該語言中,一個併發系統由若干並行運行的順序進程組成,每個進程不能對其他進程的變量賦值。進程之間只能通過 一對通信原語實現協作:Q→x表示從進程Q輸入一個值到變量x中;P<-e表示把表達式e的值發送給進程P。當P進程執行Q→x, 同時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,其選 擇不受外界影響。
[2]
- 詞條統計
-
- 瀏覽次數:次
- 編輯次數:6次歷史版本
- 最近更新: 寒927