《一种基于ＣＩＰＮ的网络协议建模方法.doc》由会员分享，可在线阅读，更多相关《一种基于ＣＩＰＮ的网络协议建模方法.doc（12页珍藏版）》请在三一文库上搜索。
1、一种基于的网络协议建模方法 (1.电子科技大学 计算机科学与工程学院，成都 610054；2.中国科学院 深圳先进技术研究院， 广东 深圳 518067) Novel CIPN-based modeling for network protocols PENG Lei1,2,BI Ya-lei2,ZENG Jia-zhi1 ?1.School of Computer Science & Engineering ,University of Electronic Science & Technology of China, Chengdu Sichuan610054, China；2.Shenz
2、hen Institute of Advanced Technology, Chinese Academy of Sciences, Shenzhen Guangdong 518067, China） Abstract:The Petri net-based modeling technique for network protocols need cooperate with existing network protocol simulators more effectively. Combing CPN and IPN together, this paper introduced a
3、novel descent of Petri net named CIPN in order to get a model highlighting the DES essence and take a formal analysis easily. Then discussed definition and operation mechanism of CIPN.Also the necessary and sufficient condition for event observability of CIPN got proofed. A MACA protocol-based examp
4、le shows that the transmission from CPN model to its equative CIPN counterpart. And analyzed the event observability of MACA with employing event observability theorem in CIPN. Key words:network protocols;discrete event system (DES);colored interpreted Petri nets (CIPN);protocol engineering ? 0引言 通信
5、协议是一类特殊的软件，工作于系统内核，空间分布性、并发性、异步性是协议运转时的主要特点。同时，通信协议为用户透明了网络，使之成为一个可靠的比特管道。因此通信协议的完整性、正确性、安全性是衡量一个通信协议设计质量的关键指标，一旦协议部署，纠正错误的代价就非常昂贵，同时也会造成用户对网络系统的极大失望。 要保证协议设计优良，必须引入规范化的方法来引导协议设计，这就是所谓的协议工程（protocol engineering, PE）1。 在继承了软件工程的一些共有理念和基本流程后，协议工程引入了形式化描述技术（formal description technique,FDT）2，贯穿于协议开发的各阶
6、段，起始于协议规范描述，以保证在协议设计过程中，可对协议进行形式化分析和求解，从而使协议的研究开发可以独立于非形式的自然语言文本和最终实现代码，避免了协议验证测试的复杂性。 形式化的协议行为分析是协议工程中非常重要的环节。一种主要的思路是基于Petri网理论对协议展开研究3，主要从协议行为和协议性能这两个方面来进行分析。协议性能分析主要对协议的网络开销、信道利用率、吞吐率等指标使用时延Petri和随机Petri进行建模分析；协议行为分析主要针对协议的设计与实现，包括对协议的容错和鲁棒性的研究，现多使用高级Petri网如着色Petri网4、层次Petri网进行建模。 目前的现状是协议工程的研究进
7、展并不理想，远远落后于软件工程。除了协议自身的特殊性， 协议工程中缺乏贯穿工程全阶段的一致模型是一大因素，这使得各阶段的工作难以环环相扣，基于Petri网的形式化分析的结论或成果难以直接指导协议的仿真与研发行为。 现在主流的协议仿真工具如NS2、OPNET的通用仿真,或如TOSSIM这种只针对于TinyOS上的WSN协议仿真，无不使用DES作为协议模型的驱动机制。因此，考虑基于DES机制构建形式化的协议行为分析网是解决上文中提出的保持模型一致性的有效方法。 IPN5是近年来Petri网的又一变种，比较适合用来构建DES系统模型，但目前的研究工作显示68：IPN受所采用的简单Petri限制，难以
8、描述类似网络协议这样的复杂系统。因此，本文提出将目前在协议行为分析中使用较多的CPN与之结合，构建出一类新的、本文命名为CIPN的Petri网派生种类，在能够较好地模拟复杂协议行为的同时还具备了较好的DES性质。 本文结合CPN和IPN给出CIPN的形式化定义，以此对CIPN的基本特性如运行和可观测性作出分析。通过一个MACA协议，展示如何从一个CPN构建等价的CIPN模型，并使用CIPN来分析MACA协议。 1CIPN的形式化定义 定义1一个CIPN由一个六元组CIPN=（CN，,O,）构成。其中： CN=(p,T;F,C,I-,I+)，为一个基本着色Petri网，但是去除了初始标记M0，C
9、N是协议活动的核心网。 =1,2,3,r，表示为DES系统信号输入表，?笑?i为输入信号，在协议活动中，该信号表示数据包到、超时触发等信号。 :T ，一个变迁命名关系，该关系需满足以下约束条件：ti,tjT,ij，pP，如果I-(p,ti)=I-(p,tj)C(0)MS同时(ti),(tj)则(ti)(tj)。为系统内部事件，在DES中为非观测事件。具体到协议活动中，关系将数据包与时间等事件与该事件的处理流程相绑定，其约束条件是表达了事件处理的惟一性。 O=(o1,o2,o3,os)，信号输出表，可描述协议活动中数据包发送、启动超时机制等信号。 :TOo，信号输出的变迁命名关系，不要求信号输出
10、的惟一性，o为null信号，该信号将不被DES观测。 ：R(CN,M0)Z+q:系统输出函数，本文使用单色托肯作为系统事件表述，此处R(CN,M0)是着色Petri网从初始标记M0开始的可达集，q为可观测信号的数目。 针对协议行为分析，系统输出函数有两种定义方式，表达了对网络协议分析的两种模式： :R(CN,M0)Oq,q=|O|，白盒模式，对协议中所有的信号进行观察。 :R(CN,M0)Oq,q=|O|,黑盒模式，与白盒模式的区别在于缩小了观测信号集。O是协议数据包，因此黑盒模式是以一种类似Sniffer窃听的方式来进行网络协议分析的。 本文假设是一个线性关系，则能以qn矩阵形式表示：=ij
11、，n=|P|。第i行分量i表示与第i个信号相关的库所单色托肯数量，ij=1M(pj)10M(pj)0。 2CIPN的形式化分析 21CIPN的运行机制 CIPN中的CN如果满足Mk(pi)tj，即pj?tjMk(pi)I-(pi,tj)。如果(tj)=n，则变迁tj将确定发生；如果(tj)=，则变迁tj以概率性发生，带有一定的不确定性，这将由CN的具体实例决定，此时系统的输出信号为yk=?Mk。当变迁tj发生时，后续标记及其输出信号为 Mk+1=Mk+AT?tj yk+1=?Mk+1 其中：AT是一个nm|R(C)MS|的立方阵，为CN的关联矩阵 ATtj=AT*1tj,AT*2tj,AT*m
12、tjT= ni=1Ai1tj(i),ni=1Ai2tj(i),ni=1Aimtj(i)T 22CIPN的事件可观测性分析 定义2CIPN中，一个变迁t在白盒模式下是可观测的，当且仅当(t)(t)o；若变迁t在黑盒模式下可观测，当且仅当(t)(t)o。 定义关系:TBoolean来表示T的可观测性。如果(t)=true，则t可观测；否则，t不可观测。 进一步，定义变迁触发语言。 定义3给定一个CIPN，定义s(CIPN)=|=titjtk,M0tiM1tjMntk，为CIPN的变迁触发语言。 基于变迁T集的可观测性，语言s被分解为可观测部分与不可观测部分：?笑摇?s, =t可通过系统的输出信号进
13、行区分，则说明该CIPN具有事件可观测性。 通过此定义，容易得到如下性质及相关定理。 性质1具有事件可观测性的CIPN不存在不可观测变迁。 定理1给定一个CIPN，该Petri网具有n个变迁，m个单色观测信号，如果该CIPN具有事件可观测性，则变迁与观测信号之间须满足不等式n3m-1。 证明tT触发时，对单色信号?笑取?(OR)（R:|）的可能影响有三种，即产生一个、消耗一个或者对没有影响，记为(1,-1,0)，因此m个观测信号可以表述3m个不同的信号序列，但一个全0的序列意味着一个不可见或者多个不可观测的变迁发生。要观测n个不同的变迁，观测信号的数量m必须满足3m-1n。 定理2一个CIPN
14、=(CN,O,)是事件可观测的，当且仅当?AT产生的列分量矩阵m=?AT*m(m=1,2,|T|)为非零矩阵且两两各异。 证明(充分性)若CIPN事件可观测，则必不存在一个不可观测变迁，因为不可观测变迁对观测信号没有影响，输出信号必然保持与前一变迁一致，或为零矩阵。对任意两个可观测变迁ti、tj而言，不失一般性，设MktiMitjMj，其输出信号为 如果?m=?j=0，则变迁tj、tm为不可观测变迁，这表明CIPN不具备事件可观测性。 这表明由tj、tm变迁引发的输出信号无法区分，该CIPN不具有事件可观测性。 3MACA协议的CIPN构建与分析 MACA协议是继CSMA/CA协议后提出的一个
15、较为完善的自组网接入控制协议。该协议提出的基于RTS/CTS控制信号能较好地避免所谓的隐藏终端和暴露终端的问题，该握手机制随后得到了广泛的应用。本文以MACA协议为样本来示例CIPN的分析方法。 31MACA的CPN模型 MACA的CPN模型假设如下： a）两节点参与，使用MACA协议进行数据收发； b）无线网络是可靠的，不引入丢包概率； c）节点RF元件可靠，不引入调制误差； d）模型中忽略数据包格式和内容； e)模型中忽略具体MAC地址。 模型如图1所示;库所定义和意义如表1所示。模型颜色集定义如下所示: 变迁意义比较明确，在此不再赘述。发送节点与接收节点通过wireless networ
16、k 库所的融合（如图1的“Fusion1”融合标记）实现模型的连接。此处，使用基于一种复合色的库所p融合和对t?p输出的弧上描述（inscription）加以限定，以及tp?加以守卫（guard）条件，能够很好地模拟网络，特别是广播式网络。该方法笔者也在文献9中使用过，得到了很好的效果。通过对该CPN模型在CPNTOOLS10中加以软件仿真运行，所得到的可达图如图2所示，各方块为MACA的系统状态，弧表示各状态间的转换路径。状态1是系统初态M0，其余各态均满足M0。例如，图2中状态6为系统状态M5，状态分量如图3所示。不难看出该标记表述了发送节点正在发送用户数据（TRANSMIT），而接收节点
17、正在准备接收数据（WFDATA）这一系统状态。 通过对状态图的遍历，MACA协议的死锁、变迁活性与家态库所等重要性质容易得到验证，本文在此不作过多描述。 尽管CPN模型已经足以用来分析MACA协议，但是该模型尚与通常意义的DES系统有一定距离，难以映射到基于DES的常用协议仿真工具，如NS2、OPNET等。因此需要对该模型扩展为CIPN。 32MACA的CIPN模型 同原始的CPN模型相比，CIPN模型（图4）增添了几个单色库所，删除了复合色的wireless network库所，但两个Petri网等价，笔者将在稍后给出证明。作为一个CIPN网络，需要定义系统的输入与输出信号/事件，及其变迁与
18、信号之间的命名关系。首先完成发送节点的 则协议MACA的系统观测信号在本例中无论采用白盒还是黑盒模式，都有 下面证明该CIPN与MACA的CPN模型的等价性： 证明若两个Petri网等价，则其可达图是同构的，并且MiR(P1,M0),MiMi,MiR(P2,M0)，Mi、Mi对系统的描述是一致的。现在MACA的CPN可达图（图2）已知，只需对MACA的CIPN计算其可达图。通过CPNTOOL的状态分析器，得到MACA的CIPN可达图如图5所示。 显而易见，CIPN的可达图与CPN的可达图同构。同时，可对可达图中每个对应的标记进行对比说明。以标记6为例：CPN和CIPN皆在发送节点的TRANSI
19、MIT库所持有1node(1)托肯，在接收节点的WFDATA库所中持有1node(2)托肯，这表明CIPN和CPN中描述的MACA协议状态一致。同理，逐个比较标记19可以发现，CIPN和CPN模型描述的MACA状态具有一致性，因此两个Petri网等价。 33MACA协议的变迁可观测性分析 首先，注意到变迁tReady对任何系统输出信号不产生影响，因此，在不引入新的系统信号下（如加上定时器信号，但必须在白盒模式下观测），触发tReady不能从系统输出信号中观测出，MACA的CIPN此时不能基于T集观测。但可以经过对发送节点的CIPN进行网归约(图6)，从而实现T集可观测性。 对于tReady，由
20、于C(?tReady)=C（t?Ready），同时tReady保持了局部的S不变量特性，归约后不会改变原CPN语意。 命题：归约tReady后的MACA的CIPN具有T集的可观测性。 证明目前使用三个单色信号RTS|CTS|USERDATA对六个变迁进行监控，显然满足T集观测性的不等式3m-1n。 显然，各分量非零且两两互异，故该CIPN为T集可观测。同理可证接收节点的CIPN的T集可观测性。 4结束语 协议工程的质量在很大程度上取决于在工程过程中抽象模型的一致性，这样才能保障协议工程各环节，特别在协议分析、验证、仿真环节的分析对象具有连贯性和一致性。在目前协议仿真工具都基于DES驱动的情况下，建立一个基于DES的协议形式化模型是保持模型一致性最为有效的方法。本文将CPN和IPN结合，提出了一种适合用于网络协议行为分析的CIPN，并对CIPN运行机制和观测性作了相应的分析。一个基于MACA协议的示例展示了如何从一个CPN模型构造一个与之等价的CIPN模型，并使用CIPN的事件可观测性定理对该模型进行了事件可观测性分析。具有事件可观测性的Petri网模型能够较为容易地转换为通用协议仿真工具中的对应模型，如OPNET的Process模型，在保持模型一致的基础上可以实现对协议行为和性能的同步分析。