基于MWB的通信系統(tǒng)演算CCS的模型檢測論文
基于MWB的通信系統(tǒng)演算CCS的模型檢測論文
通信系統(tǒng)是用以完成信息傳輸過程的技術(shù)系統(tǒng)的總稱。現(xiàn)代通信系統(tǒng)主要借助電磁波在自由空間的傳播或在導(dǎo)引媒體中的傳輸機(jī)理來實現(xiàn)，前者稱為無線通信系統(tǒng)，后者稱為有線通信系統(tǒng)。以下是學(xué)習(xí)啦小編今天為大家精心準(zhǔn)備的：基于MWB的通信系統(tǒng)演算CCS的模型檢測相關(guān)通信工程論文。內(nèi)容僅供參考，歡迎閱讀!
基于MWB的通信系統(tǒng)演算CCS的模型檢測全文如下：
一、通信系統(tǒng)演算CCS
Robin Milner在上世紀(jì)70年代論文范文首先提出了描述通信系統(tǒng)并發(fā)行為的形式演算CCS(Calculus of Communicating Systems，[1])，可以對并發(fā)系統(tǒng)進(jìn)行推理，是進(jìn)程代數(shù)(process algebra)領(lǐng)域的開拓性工作，在CCS的基礎(chǔ)上，建立了通信序列演算CSP，π演算、spi演算、應(yīng)用π演算、環(huán)境(Ambient)演算等一大批描述分布式移動并發(fā)系統(tǒng)的形式方法。
1.1 CCS的語法
CCS的基本成分是事件(或動作，Action)與進(jìn)程;CCS的事件分為兩類，一類用來描述進(jìn)程間通信的同步動作： = {a,b,c ,…}為輸入事件集，相應(yīng)的 ’ = {’a,’b,’c ,…}為輸出事件集;用t表示非交互事件(進(jìn)程內(nèi)部事件)集。記ACCS= ’ {t};LACCS
CCS的進(jìn)程P如下定義：
P : := .P 前綴，ACCS
P1 | P2 并發(fā)
iIPi 選擇，這里I為有窮集
(^L)P 限制，這里L(fēng) ACCS
P[f] 改名，這里f是從ACCS到ACCS的映射并滿足：f(t)=t，f(’)=’f()
記 PCCS為CCS的一切進(jìn)程的集合，記P1+P2=i{1,2}Pi，記0(或Nil)=iPi;為減少 號，約定運(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將寫為=。
.......................
二、移動工作臺MWB(Mobility Workbench)
2.1 移動工作臺MWB(Mobility Workbench)是針對-演算開發(fā)的第一個自動驗證工具[VM94]，可對用-演算[2、3、4]、通信系統(tǒng)演算CCS[1]描述的移動并發(fā)系統(tǒng)進(jìn)行分析與驗證;MWB首先在瑞典的Uppsala大學(xué)開發(fā)[5、6、7];可在Windows、Linux等系統(tǒng)下使用，MWB是開放源代碼的，可從下面網(wǎng)址下載：
2.2 在Windows2000下安裝使用
由于MWB是用語言ML寫成, 需要在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
并寫一個批處理文件mwb.bat，內(nèi)容為：
sml @SMLload=mwb.x86-win32
將mwb.x86-win32與mwb.bat放到一個目錄，點擊mwb.bat即可運(yùn)行MWB。
2.3 CCS公式的MWB編碼
為將CCS公式輸入MWB，需將通常的CCS公式做一些轉(zhuǎn)換：將受限名字P\L用(^L)P表示;對任何P，設(shè)P的自由名字(非受限名字)為a1,…,ai，在MWB中，用ID(a1,…,ai)來表示P為：
agent ID(a1,…ai) = P
ID稱為P的名，注意P的名可用任意的符號串(例如MyID或者P)，但第一個字母需大寫，且(…)里一定要將P的非受限名字完全列舉;例如：設(shè)P遞歸定義為ã.b.P，可寫成MWB式子為
agent P(a,b) = ‘a.b.P
不能寫成：agent P = ‘a.b.P;可將幾個MWB公式放到一塊以ag為擴(kuò)展名用ASCII文件存盤.
..............................
三、交替比特協(xié)議ABP的MWB分析
我們討論簡單AB協(xié)議：設(shè)S為發(fā)送方、R為接受方;S發(fā)出報文(’m)或超時(timeout)重發(fā)報文;R接到報文發(fā)現(xiàn)報文錯誤則丟棄報文(down)，否則通知S已收到(ack);ABP=S|R描述了這個簡單的交換比特協(xié)議，其中：
S=’m.S1
S1=timeout.’m.S1+ack.S
R=m.(down.R+’ack.R)
S1中的timeout.’m.S1表示報文超時重發(fā)，而ack.S表示S接到R的肯定回復(fù)后交替比特再發(fā)報文;R中的down.R表示發(fā)現(xiàn)報文錯誤丟棄報文，’ack.R通知S已收到;進(jìn)程ABP=S|R描述了這個簡單的交換比特協(xié)議;將上述CCS描述用MWB格式書寫并以abp1.ag存盤：
...............
參考文獻(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]古天龍,蔡國勇. 網(wǎng)絡(luò)協(xié)議的形式化分析與設(shè)計，電子工業(yè)出版社，2003