基于MWB的通信系统演算CCS的模型测试论文
通信系统是用以完成信息传输过程的技术系统的总称。现代通信系统主要借用电磁波在自由空间的传播或在导引媒体中的传输机理来达成，前者称为无线通信系统，后者称为有线通信系统。以下是学习啦我们今天为大伙精心筹备的：基于MWB的通信系统演算CCS的模型测试有关通信工程论文。内容仅供参考，欢迎阅读!
基于MWB的通信系统演算CCS的模型测试全文如下：
1、通信系统演算CCS
Robin Milner在上世纪70年代论文范本第一提出了描述通信系统并发行为的形式演算CCS，可以对并发系统进行推理，是进程代数范围的发展性工作，在CCS的基础上，打造了通信序列演算CSP，演算、spi演算、应用演算、环境演算等一大量描述分布式移动并发系统的形式办法。
1.1 CCS的语法
CCS的基本成分是事件与进程;CCS的事件分为两类，一类用来描述进程间通信的同步动作： = {a,b,c ,}为输入事件集，相应的 = {a,b,c ,}为输出事件集;用t表示非交互事件集。记ACCS= {t};LACCS
CCS的进程P如下概念：
P : := .P 前缀，ACCS
P1 | P2 并发
iIPi 选择，这里I为有穷集
P 限制，这里L ACCS
P[f] 改名，这里f是从ACCS到ACCS的映射并满足：f=t，f=f
记 PCCS为CCS的所有进程的集合，记P1+P2=i{1,2}Pi，记0=iPi;为降低 号，约定运算顺序为：^ , | , +;比如 R+a.P|b.Q是R+|Q))
在CCS中，大家引入A =df P，即用CCS进程P概念A;在CCS里可以进行递归概念，比如：A =df a.A|P，在不引起混乱的状况下，可将=df将写为=。
.......................
2、移动工作台MWB
2.1 移动工作台MWB是针对-演算开发的第一个自动验证工具[VM94]，可对用-演算[2、3、4]、通信系统演算CCS[1]描述的移动并发系统进行剖析与验证;MWB第一在瑞典的Uppsala大学开发[5、6、7];可在Windows、Linux等系统下用，MWB是开放源码的，可从下面网址下载：
2.2 在Windows2000下安装用
因为MWB是用语言ML写成, 需要在New Jersey SML 编译器下运行;从下列网址下载smlnj：
获得smlnj.exe，可自解压并装配到C:\sml;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用P表示;对任何P，设P的自由名字为a1,,ai，在MWB中，用ID来表示P为：
agent ID = P
ID称为P的名，注意P的名可用任意的符号串，但第一个字母需大写，且里必须要将P的非受限名字完全列举;比如：设P递归概念为.b.P，可写成MWB式子为
agent P = a.b.P
不可以写成：agent P = a.b.P;可将几个MWB公式放到一块以ag为扩展名用ASCII文件存盘.
..............................
3、交替比特协议ABP的MWB剖析
大家讨论容易AB协议：设S为发送方、R为同意方;S发出报文或超时重发报文;R接到报文发现报文错误则遗弃报文，不然公告S已收到;ABP=S|R描述了这个容易的交换比特协议，其中：
S=m.S1
S1=timeout.m.S1+ack.S
R=m.
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 Users 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 CAV94, Lecture Notes in Computer Science. Springer-Verlag, 1994.
[10]古天龙,蔡国勇. 互联网协议的形式化剖析与设计，电子工业出版社，2003
