基于MWB的通信系統(tǒng)演算CCS的模型檢測(cè)論文

　　通信系統(tǒng)是用以完成信息傳輸過(guò)程的技術(shù)系統(tǒng)的總稱(chēng)?，F(xiàn)代通信系統(tǒng)主要借助電磁波在自由空間的傳播或在導(dǎo)引媒體中的傳輸機(jī)理來(lái)實(shí)現(xiàn)，前者稱(chēng)為無(wú)線(xiàn)通信系統(tǒng)，后者稱(chēng)為有線(xiàn)通信系統(tǒng)。以下是學(xué)習(xí)啦小編今天為大家精心準(zhǔn)備的：基于MWB的通信系統(tǒng)演算CCS的模型檢測(cè)相關(guān)通信工程論文。內(nèi)容僅供參考，歡迎閱讀!

　　基于MWB的通信系統(tǒng)演算CCS的模型檢測(cè)全文如下：

　　一、通信系統(tǒng)演算CCS

　　Robin Milner在上世紀(jì)70年代論文范文首先提出了描述通信系統(tǒng)并發(fā)行為的形式演算CCS(Calculus of Communicating Systems，[1])，可以對(duì)并發(fā)系統(tǒng)進(jìn)行推理，是進(jìn)程代數(shù)(process algebra)領(lǐng)域的開(kāi)拓性工作，在CCS的基礎(chǔ)上，建立了通信序列演算CSP，π演算、spi演算、應(yīng)用π演算、環(huán)境(Ambient)演算等一大批描述分布式移動(dòng)并發(fā)系統(tǒng)的形式方法。

　　1.1 CCS的語(yǔ)法

　　CCS的基本成分是事件(或動(dòng)作，Action)與進(jìn)程;CCS的事件分為兩類(lèi)，一類(lèi)用來(lái)描述進(jìn)程間通信的同步動(dòng)作： = {a,b,c ,…}為輸入事件集，相應(yīng)的 ’ = {’a,’b,’c ,…}為輸出事件集;用t表示非交互事件(進(jìn)程內(nèi)部事件)集。記ACCS=  ’  {t};LACCS

　　CCS的進(jìn)程P如下定義：

　　P : := .P 前綴，ACCS

　　P1 | P2 并發(fā)

　　iIPi 選擇，這里I為有窮集

　　(^L)P 限制，這里L(fēng) ACCS

　　P[f] 改名，這里f是從ACCS到ACCS的映射并滿(mǎn)足：f(t)=t，f(’)=’f()

　　記 PCCS為CCS的一切進(jìn)程的集合，記P1+P2=i{1,2}Pi，記0(或Nil)=iPi;為減少 號(hào)，約定運(yùn)算順序?yàn)椋篰 , | , +;例如 R+a.P|b.(^L)Q是R+((a.P)|(b.(^L)Q))

　　在CCS中，我們引入A =df P，即用CCS進(jìn)程P定義A;在CCS里可以進(jìn)行遞歸定義，例如：A =df a.A|P，在不引起混亂的情況下，可將=df將寫(xiě)為=。

　　.......................

　　二、移動(dòng)工作臺(tái)MWB(Mobility Workbench)

　　2.1 移動(dòng)工作臺(tái)MWB(Mobility Workbench)是針對(duì)-演算開(kāi)發(fā)的第一個(gè)自動(dòng)驗(yàn)證工具[VM94]，可對(duì)用-演算[2、3、4]、通信系統(tǒng)演算CCS[1]描述的移動(dòng)并發(fā)系統(tǒng)進(jìn)行分析與驗(yàn)證;MWB首先在瑞典的Uppsala大學(xué)開(kāi)發(fā)[5、6、7];可在Windows、Linux等系統(tǒng)下使用，MWB是開(kāi)放源代碼的，可從下面網(wǎng)址下載：

　　2.2 在Windows2000下安裝使用

　　由于MWB是用語(yǔ)言ML寫(xiě)成, 需要在New Jersey SML 編譯器(Standard ML of New Jersey - SML/NJ，目前最新的版本是smlnj-110.54)下運(yùn)行;從下列網(wǎng)址下載smlnj：

　　獲得smlnj.exe，可自解壓并裝配到C:\sml(我們使用的版本是：Standard ML of New Jersey 110.0.7);SML/NJ安裝成功后，從下列網(wǎng)址下載mwb.x86-win32

　　并寫(xiě)一個(gè)批處理文件mwb.bat，內(nèi)容為：

　　sml @SMLload=mwb.x86-win32

　　將mwb.x86-win32與mwb.bat放到一個(gè)目錄，點(diǎn)擊mwb.bat即可運(yùn)行MWB。

　　2.3 CCS公式的MWB編碼

　　為將CCS公式輸入MWB，需將通常的CCS公式做一些轉(zhuǎn)換：將受限名字P\L用(^L)P表示;對(duì)任何P，設(shè)P的自由名字(非受限名字)為a1,…,ai，在MWB中，用ID(a1,…,ai)來(lái)表示P為：

　　agent ID(a1,…ai) = P

　　ID稱(chēng)為P的名，注意P的名可用任意的符號(hào)串(例如MyID或者P)，但第一個(gè)字母需大寫(xiě)，且(…)里一定要將P的非受限名字完全列舉;例如：設(shè)P遞歸定義為ã.b.P，可寫(xiě)成MWB式子為

　　agent P(a,b) = ‘a.b.P

　　不能寫(xiě)成：agent P = ‘a.b.P;可將幾個(gè)MWB公式放到一塊以ag為擴(kuò)展名用ASCII文件存盤(pán).

　　..............................

　　三、交替比特協(xié)議ABP的MWB分析

　　我們討論簡(jiǎn)單AB協(xié)議：設(shè)S為發(fā)送方、R為接受方;S發(fā)出報(bào)文(’m)或超時(shí)(timeout)重發(fā)報(bào)文;R接到報(bào)文發(fā)現(xiàn)報(bào)文錯(cuò)誤則丟棄報(bào)文(down)，否則通知S已收到(ack);ABP=S|R描述了這個(gè)簡(jiǎn)單的交換比特協(xié)議，其中：

　　S=’m.S1

　　S1=timeout.’m.S1+ack.S

　　R=m.(down.R+’ack.R)

　　S1中的timeout.’m.S1表示報(bào)文超時(shí)重發(fā)，而ack.S表示S接到R的肯定回復(fù)后交替比特再發(fā)報(bào)文;R中的down.R表示發(fā)現(xiàn)報(bào)文錯(cuò)誤丟棄報(bào)文，’ack.R通知S已收到;進(jìn)程ABP=S|R描述了這個(gè)簡(jiǎn)單的交換比特協(xié)議;將上述CCS描述用MWB格式書(shū)寫(xiě)并以abp1.ag存盤(pán)：

　　...............

　　參考文獻(xiàn)

　　[1] MWB軟件：

　　[2] Robin Milner. The polyadic www.51lunwen.com/communication/ -calculus: A tutorial. Technical Report ECS-LFCS-91-180, LFCS, Department of Computer Science, University of Edinburgh, 1991.

　　[3] Robin Milner. Communicating and Mobile Systems: the -calculus. Cambridge University Press, 1999.

　　[4] Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, parts I and II. Journal of Information and Computation, 100:1-40 and 41-77, 1992.

　　[5] Robin Milner. Communication and Concurrency. Prentice-Hall, 1989.

　　[6] Bjorn Victor. A Verification Tool for the Polyadic -Calculus. Licentiate thesis, Department of Computer Systems, Uppsala University, 1994. Available as report DoCS 94/50.

　　[7] Bjorn Victor. The Mobility Workbench User's Guide: Polyadic version 3.122. Department of Information Technology, Uppsala University, 1995.

　　[8] Bjorn Victor and Faron Moller. The mobility workbench : a tool for the -calculus. Technical Report DoCS 94/45, Department of Computer Systems, Uppsala University, 1994. Also available as Technical Report ECS-LFCS-94-285, Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh.

　　[9] B. Victor and F. Moller. The Mobility Workbench - a tool for the pi-calculus. In D. Dill, editor, Proceedings of CAV'94, Lecture Notes in Computer Science. Springer-Verlag, 1994.

　　[10]古天龍,蔡國(guó)勇. 網(wǎng)絡(luò)協(xié)議的形式化分析與設(shè)計(jì)，電子工業(yè)出版社，2003