複製鏈接
請複製以下鏈接發送給好友

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] 
參考資料
  • 1.    範紅,馮登國,安全協議理論與方法 [M]
  • 2.    C. A. R Hoare.Communicating sequential processes[M].London:Prentice/Hall International,1985.ISBN: 9780131532717