基于MWB的通信系統演算CCS的模型檢測論文

基于MWB的通信系統演算CCS的模型檢測論文

　　通信系統是用以完成信息傳輸過程的技術系統的總稱。現代通信系統主要借助電磁波在自由空間的傳播或在導引媒體中的傳輸機理來實現，前者稱為無線通信系統，后者稱為有線通信系統。以下是學習啦小編今天為大家精心準備的：基于MWB的通信系統演算CCS的模型檢測相關通信工程論文。內容僅供參考，歡迎閱讀!

　　基于MWB的通信系統演算CCS的模型檢測全文如下：

　　一、通信系統演算CCS

　　Robin Milner在上世紀70年代論文范文首先提出了描述通信系統并發行為的形式演算CCS(Calculus of Communicating Systems，[1])，可以對并發系統進行推理，是進程代數(process algebra)領域的開拓性工作，在CCS的基礎上，建立了通信序列演算CSP，π演算、spi演算、應用π演算、環境(Ambient)演算等一大批描述分布式移動并發系統的形式方法。

　　1.1 CCS的語法

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

　　CCS的進程P如下定義：

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

　　P1 | P2 并發

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

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

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

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

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

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

　　二、移動工作臺MWB(Mobility Workbench)

　　2.1 移動工作臺MWB(Mobility Workbench)是針對-演算開發的第一個自動驗證工具[VM94]，可對用-演算[2、3、4]、通信系統演算CCS[1]描述的移動并發系統進行分析與驗證;MWB首先在瑞典的Uppsala大學開發[5、6、7];可在Windows、Linux等系統下使用，MWB是開放源代碼的，可從下面網址下載：

　　2.2 在Windows2000下安裝使用

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

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

　　并寫一個批處理文件mwb.bat，內容為：

　　sml @SMLload=mwb.x86-win32

　　將mwb.x86-win32與mwb.bat放到一個目錄，點擊mwb.bat即可運行MWB。

　　2.3 CCS公式的MWB編碼

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

　　agent ID(a1,…ai) = P

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

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

　　不能寫成：agent P = ‘a.b.P;可將幾個MWB公式放到一塊以ag為擴展名用ASCII文件存盤.

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

　　三、交替比特協議ABP的MWB分析

　　我們討論簡單AB協議：設S為發送方、R為接受方;S發出報文(’m)或超時(timeout)重發報文;R接到報文發現報文錯誤則丟棄報文(down)，否則通知S已收到(ack);ABP=S|R描述了這個簡單的交換比特協議，其中：

　　S=’m.S1

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

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

　　S1中的timeout.’m.S1表示報文超時重發，而ack.S表示S接到R的肯定回復后交替比特再發報文;R中的down.R表示發現報文錯誤丟棄報文，’ack.R通知S已收到;進程ABP=S|R描述了這個簡單的交換比特協議;將上述CCS描述用MWB格式書寫并以abp1.ag存盤：

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

　　參考文獻

　　[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]古天龍,蔡國勇. 網絡協議的形式化分析與設計，電子工業出版社，2003