第3章-协议形式化描述技术(2-PetriNet).ppt

《第3章-协议形式化描述技术(2-PetriNet).ppt》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、第3章协议形式化描述技术（2-PetriNet）内容提要概述1PetriNet的扩充2PetriNet性质3在协议描述中的应用42PetriNet(PN)德国学者C.A.Petri于1962年在其博士论文《用自动机通信》中首次提出的一种特殊的自动机模型,后来被称为Petri网。Petri网也是一种状态变迁模型，它允许同时发生多个状态变迁，因而Petri网是一种并发模型。Petri网适合于并发、异步、分布式系统描述与分析的图形数字工具，可用来描述通信系统中各异步成分之间的关系，已被广泛应用于计算机科学、电子学、机械学、化学、物理学

2、等许多领域。3PetriNet:FormalDefinitionPetri网可定义为一个4元组(P,T,I,O)，其中：P={p1,p2,…,pn}是位置(places)的有限集合；T={t1,t2,…,tm}是变迁(transitions)的有限集合，且T与P不相交，即T∩P=。I是输入函数，是变迁T到位置的映射。对于每一个tk∈T，可得出相应的I(tk)={pi,pj,…}。O是输出函数，也是一种变迁T到位置的映射。对于每一个tk∈T，可以得出相应的O(tj)={pr,ps,…}。也有文献将其定义为5元组：(P,T,I,O，

3、M)M={m1,m2,…,mn}是标记(tokens,“旗标”或“托肯”)的集合4PetriNet:RepresentationUsingGraphp1p2p3p4p5t1t2t3··位置标记。每个位置中有0个或多个标记Petri所处的状态是由标记的分布来决定：在位置pi中的标记个数常i来表示。上图中，1=2，2=3=4=5=0也可以用向量=(1,2,…,n)来表示整个Petri网的标记分布情况。可以看出，现在=(2,0,0,0,0)。位置的名称变迁变迁名称5PetriNet:状态变迁(Transitions

4、)发生变迁的条件：必须有1个或多个变迁满足变迁条件。变迁条件就是某个变迁tj的所有输入位置中都必须有标记存在，并且当输入位置有多根弧线指向这个变迁时，该输入位置也至少具有和弧线根数相等的标记数。如，上图中的t1必须发生点火(firing)。所谓点火就是发生了一些事件(1个或多个)，而这些事件所对应的变迁满足变迁条件。发生点火后，标记要重新分布。标记移动规则是：从点火的变迁tj所有输入位置中均取出标记，每个位置取出的标记数等于该位置指向点火的tj的弧线数；然后再将标记送入tj的所有输出位置中去，送入每个位置的标记数等于点火的tj指向

5、该位置的弧线数。6PetriNet:状态变迁例子p1p2p3p4p5t1t2t3··=(2,0,0,0,0)=(1,1,1,1,0)p1p2p3p4p5t1t2t3····t1发生点火后7PetriNet:状态变迁例子（Cont.）=(1,1,1,1,0)p1p2p3p4p5t1t2t3····t1再次发生点火后=(0,2,2,2,0)t2开始具备点火条件p1p2p3p4p5t1t2t3······8PetriNet:状态变迁例子（Cont.）=(0,2,2,2,0)t2发生点火后=(0,2,1,0,0)

6、不能再发生任何点火p1p2p3p4p5t1t2t3···p1p2p3p4p5t1t2t3······9PetriNet:状态变迁类型顺序变迁。如图(a)所示。只有当t1点火后t2才能点火。并发变迁，如图(b)所示。t1和t2可同时(当然也可以单独)点火。互斥变迁，如图(c)所示。t1和t2中只能有一个点火。一个点火后另一个就不能再点火了。t1t2···t1t2··t1t2·(a)(b)(c)10内容提要概述1PetriNet的扩充2PetriNet性质3在协议描述中的应用411PetriNet的扩充为适应不同规范描述及验证的需求，

7、从基本Petri网模型衍化出许多扩展模型系统，如谓词/动作Petri网、时间Petri网（TimePetriNet）、带时态逻辑的Petri网、有色Petri网（ColouredPetriNet）、面向对象Petri网(OOPN)、随机Petri网（StochasticPetriNet）、数字Petri网（NPN）......12PetriNet的扩充（续）主要从以下几个方面来扩充基于标记和位置的扩充基于输入函数和输出函数的扩充基于变迁的扩充13基于位置和标记的扩充在标准的Petri网中，所有的标记都是一样的，没有名字。如果我们将

8、一个位置中的不同标记用不同的名字或标识号来表示，就可以大大扩充标记的表达能力。这种有名标记的Petri就是有色Petri网(ColorPetriNet)例如，如果位置中的标记表示系统资源时，名字不同的标记就可表示不同的资源。同样，如果用标记表示报文