基于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