形式化开发方法-Petri网.ppt_第1页
形式化开发方法-Petri网.ppt_第2页
形式化开发方法-Petri网.ppt_第3页
形式化开发方法-Petri网.ppt_第4页
形式化开发方法-Petri网.ppt_第5页
已阅读5页,还剩136页未读 继续免费阅读

下载本文档

版权说明:本文档由用户提供并上传,收益归属内容提供方,若内容存在侵权,请进行举报或认领

文档简介

1、软件工程形式化方法,第5章 形式化开发方法(1),-3-,内容安排,软件开发的形式化方法 形式化开发方法(1) Petri网 形式化开发方法(2) 时态逻辑 形式化开发方法(3) Z方法,-4-,软件开发的形式化方法,软件开发的形式化方法定义 软件开发的形式化方法(formal methods)是建立在严格数学基础上,具有精确数学语义的开发方法 简单地说,凡在系统研究中,应用了数学的方法,都是形式化方法 本章所介绍的形式化开发方法是指软件规格说明数学建模、数学验证和数学程序求精,-5-,形式化方法与结构化和OO方法区别,结构化和OO方法 使用了大量的自然语言。自然语言的二义性、不完整和抽象层次

2、的混杂等问题的解决,必然使开发系统的质量不高、成本增加和进度拖长;尤其对安全性或其他质量因素要求极高的软件,任何微小的错误都可能带来灾难性的后果 形式化的方法 可以帮助软件开发人员开发出更为无二义性、完整的和准确的需求规格说明,进而通过严格的验证发现问题,以达到对软件质量、开发成本和开发进度的有效控制,-6-,形式化开发方法发展历史,20世纪60年代末 形式化方法与非形式化大致同步 都是为解决当时出现的“软件危机”提出 一般认为是Floyd、Hoare和Manna等在程序正确性证明方面的研究。但由于这些方法受程序规模的限制而未能应用 20世纪80年代末 在硬件设计领域形式化方法的工业应用结果,

3、又掀起了软件形式化开发方法的学术研究和工业应用的热潮,建立了一些较为成熟的方法和语言 如Petri网、statecharts、通信顺序过程、通信系统演算、程序正确性证明、时态逻辑、模型验证、Z语言、 VDM及Larch等,-7-,目前流行的形式化开发方法,形式化规格说明建模 形式化验证 形式化程序求精,-8-,形式化规格说明建模,操作类 基于状态和转移 Petri网、有限状态机和状态图 描述类 基于数学公理和概念 基于逻辑的描述方法:命题线性时态逻辑(PLTL)、一阶线性时态逻辑(FOLTL)、计算树逻辑(CTL) 基于代数的描述方法:Z语言、VDM和Larch 双重类 兼有操作类和描述类两者

4、的特点 扩展状态机(ESM)、实时时态逻辑(RTTL),-9-,形式化验证,模型验证和定理证明 模型验证是对规格说明所建立起来的模型状态空间进行搜索,以确认该系统模型是否具有所期望的某些性质 定理证明是以逻辑公式作为系统及其性能的规格说明,其中逻辑由一个具有公理和推理规则的形式化系统给出。进行定理证明的过程就是应用这些公理或推理规则来证明系统是否具有所期望的性质,-10-,形式化程序求精,形式化程序求精就是将自动推理与形式化规格说明相结合而形成的一门技术 研究如何从形式化的规格说明推演出具体的面向计算机的程序代码的全过程 基本思想就是用一个抽象程度低和过程性强的程序,去代替一个抽象程度高和过程

5、性弱的程序,并保证它们的功能和性质完全一致 形式化程序求精与形式化规格说明和形式化验证三者是紧密联系和相辅相成,-11-,形式化开发方法主要问题,对软件开发人员(包括管理人员和用户)的数学素质有较高的要求 主要是离散数学中的集合、代数结构、数理逻辑等基础内容在软件工程中的具体应用 对于原来一些数学背景较差的工程人员要花许多时间去学习和掌握。有的甚至还要克服对数学的畏惧心理 在选择和应用形式化开发方法时应注意的问题 Bowan和Hinchley提出了“形式化法方法的十条戒律”,-12-,形式化开发方法(1) Petri网,-13-,什么是Petri网 Petri网是一种网状结构的系统的描述和分析

6、工具 对于具有并发、异步、分布、并行、不确定性或随机性的信息系统,都可以利用这种工具构造出要开发的Petri网模型。然后对其进行分析,即可得到有关系统结构和动态行为方面的信息。根据这些信息就可以对要开发的系统进行评价和改进 Petri网的提出 由德国C.A. Petri在他的62年博士论文“Communication with automata”中提出 当时引起一些欧美科学家的重视。他们在引用这种网状结 构模拟和分析并行系统中称它为“Petri Nets”。从此以后大家都称它为Petri网,-14-,Petri网介绍的内容,示例-四季系统 Petri网的定义 Petri网的基本原理-静态结构

7、Petri网的基本原理-动态特征 建模实例 特性分析 Petri网的特性分析方法 改进Petri网及其应用 时间网和随机网 从Petri网到程序结构的转换,-15-,示例:四季系统,一年有四季,四季气候的变化,该系统可以由图形表示,-16-,系统的Petri网图形表示,-17-,系统的Petri网数学表示,=(P,T;F,M0) P=p1, p2, p3, p4 T=t1, t2, t3, t4 F=(p1, t1), (t1, p2), (p2, t2), (t2, p3), (p3, t3), (t3, p4), (p4, t4), (t4, p1) M0=(0, 0, 0, 1),-18

8、-,Petri网描述系统的特点,从四季系统中,可以看出这种利用事物的因果关系对系统进行网状结构的描述,有以下特点 自然 没有任何不必要的人为控制,完全反映了现实世界的真实情况 局部确定原理 因为事件或转移的发生和结果都由局部状态决定 既有系统静态结构,又有动态行为方面的信息 既有图形工具,又有数学工具 图形工具和数学工具完全等价 图形工具直观、形象、易懂、易学;数学工具严谨,既便于计算,又便于验证,-19-,Petri网的基本原理:静态结构,任何系统都有两类元素组成:表示状态的元素和表示状态变化的元素 Petri网 位置(place):状态 转移(transition):改变状态 两者之间的依

9、赖关系用弧(箭头)表示,-20-,Petri网的基本成分(1),-21-,Petri网的基本成分(2),其中: P=(p1,p2, ,pm)是N的有穷位置集合, T=(t1,t2,tn )是N的有穷转移集合, F是由N中一个P元素和一个T元素组成的有序偶的集合,F称为流关系。(PT)和(TP)中的“ ”为笛卡尔乘积。 DOM(F)=x y:(x,y) F,COD(F)= x y:(y,x F分别为F所含的有偶序偶的第一个元素组成的集合和第二个元素组成的集合。,-22-,Petri网的基本成分(3),由上可以说明 N=(P,T;F)是位置集合P和转移集合T构造Petri网的两个基本成分,P与T两

10、者间的流关系F是从它们构造出来的。所以在P、T之后的F用分号“;”隔开来 PT 说明网中至少要有一个元素,PT= 说明P和T为两类不同的元素,两者不能有交 F (PT) (TP)说明一个P元素代表一个资源,其流动由F关系规定。所以,转移T只能与位置有直接的流关系,不是从PT,就是从T P。而不参与任何转移的资源为孤立的P,不引起资源流动的转移为孤立的T。所以DOM(F) COD(F)=P T说明网中不能有孤立的元素P或T,-23-,前集、后集、子网,设 ,令 *x=y|(y, x)F, x*=y|(x, y)F *x被称为x的前集或输入集。 x*被称为x的后集或输出集。 在N1=(P1,T1;

11、F1)和N2=(P2,T2;F2)中, 如果 , , 且 , 则称N1是N2的子网。,-24-,纯网,在N=(P,T;F)中,如果对似有xPT,都有*x x*= ,则称N为纯网(pure net) 纯网中无公共前后集(环),-25-,简单网,如果对所有x,yPT,都有(*x= *y) (x*=y*) x=y,则称N为简单网(simple net) 简单网中无相同的前后集,-26-,Petri网的基本原理:动态特征(1),Petri网作为系统的建模工具,除具有上述描述的静态结构外,还应包括位置的容量和转移发生对位置容量的影响信息。有限容量可用大于零的整数表示,转移发生对位置中标记数的影响用孤上的

12、整数表示。于是,具有动态特征的Petri网可表示为六元组:,-27-,Petri网的基本原理:动态特征(2),Petri网的六元组: 其中: (P,T;F)含义同前 K:PN 是位置上的容量函数,N= 0,1,2,3, ,若K(p)= ,表示位置中的容量为无穷 W:F N是孤集合上的孤函数 M:P N0是Petri网的标识(marking)。M0为初始标识, N0=0,1,2,3, , pP,必须满足M(p) K(p) 在Petri网的图形表示中,M(p)不是用数字,而是用实圆点表示。每个实圆点为一个标记,同一个位置中的诸多标记代表同一类完全等价的个体。弧(x,y)上的W值标注在孤(x,y)上

13、,-28-,转移发生规则(1),Petri网的动态行为是通过转移发生引起标识改变来体现的 转移可发生的条件和发生规则 转移t 可发生的条件 若在标识M下, p1, p1*t M(p1) (p1,t), 且p2, p2 t* M(p2)+W(t, p2) K(p2)+W(t, p2) K(p2),此时称t在M 下可发生,记为M t 转移t发生的结果 若t在M下可发生, 就可以发生, 发生后将M 变成新标识M,出视方出记为MtM 或M M,并称M 为M 的后继标识 对p P, M(p)=M(p)W(p,t) 当p* t t * =M(p)W(t,p) 当pt * * t =M(p) W(p,t)

14、W(t,p) 当p * t t * =M(p) 当pt * * t,-29-,转移发生规则(2),注意 一个没有任何输入位置的转移叫源转移,一个源转移的可发生是无条件的。一个源转移的发生只会产生标记,而不消耗任何标记 一个没有任何输出位置的转移叫潭转移,一个潭转移的发生将消耗标记,而不产生任何标记,-30-,示例:转移发生规则,以本例来说明网论中的转移发生规则,以及网论中的冲突(conflict)、并发(concurrent)和碰撞(contact)现象 有时,一个Petri网中同时存在并发和冲突,而且并发的发生会引起冲突的消失或出现。网论中称这种现象为混惑(confusion),-31-,并

15、发和冲突概念的完整描述,并发 设M 为Petri网的一个标识,若存在t1和t2使得M t1 和M t2 ,并满足 ,且则称t1和t2 在M 下并发 冲突 设M 为Petri网的一个标识,若存在t1和t2使得M t1 和M t2 ,并满足 ,且则称t1 和t2 在M 下冲突,-32-,网系统分类,根据Petri网系统中容量函数K和权函数W的不同可分为三种情况 K1,W1 为基本网(elementary net,EN)系统 这种网系统位置p 中,只有有标记和无标记两种状态。习惯上把这种网称为条件/ 转移网系统 K,W1 为P/T(place/transition)网 K和W为任意函效 为P/T系统

16、 P/T网和P/T系统中都是物质资源,它们与EN系统有本质的不同。所以,EN系统又叫做条件/事件网系统。 P/T网和P/T系统也有区别。K(p)(位置容量)是其能容纳此类资源的能力,也称空间资源。而W(p,t)和W(t,p)分别是转移t 发生时释放和占用此类空间资源的数量。P/T网的位置p 容量足够大,所以不会发生碰撞。而P/T系统,如果位置p 容量有限,且不进行技术处理,则有可能发生碰撞,-33-,Petri网转移发生规则的简化,对Petri网简化的原因是为了对Petri网进行理论上研究的方便 通过上面讨论可以看出,对于简单的Petri网,由于K和W已无任何限制作用。所以,一般把这种Petr

17、i网系统记为:=(N,M)=(P,T;F,M)。这种Petri网系统的转移发生规则,可以简化为: 若Mt,当且仅当p p,M (p) 1,t 发生后,Mt M M (p)=M (p) 1 当 p * t t * =M (p) 1 当 p t * * t =M (p) 其它 网论可以证明,经过适当加技术处理,都可以把K、W任意的P/T网或P/T系统改造为K ,W 1的Petri网 M(p)=M(p) 1 当p * t t * =M(p) 1 当p t * * t =M(p) 其它,-34-,建模实例:有限状态机,-35-,建模实例:并行活动,-36-,建模实例:数据流计算,-37-,建模实例:通

18、信协议,-38-,建模实例:同步控制,-39-,建模实例:生产者/消费者系统(1),-40-,建模实例:生产者/消费者系统(2),抑制弧,-41-,建模实例:形式语言,-42-,建模实例:机械加工(1),-43-,建模实例:机械加工(2),-44-,建模实例:机械加工(3),-45-,建模实例:机械加工(4),-46-,建模实例:机械加工(5),-47-,特性分析,Pretri网的特性主要包括 可达性(Reachability) 有界性(Boundedness) 活性(Liveness) 可逆性(Reversibility) 可覆盖性(Coverability) 持久性(Persistence

19、) 同步距离(Synchronic Distance) 公平性(Fairness),-48-,特性分析-可达性,对Petri网(N,M0),如果存在一个从M0到Mn的发生序列,则称标识Mn是从M0可达的。发生序列表示为= M0t1M1t2M2t3M3tnMn,或简化为 =t1t2tn。 可用M0 Mn 表示三者间的关系。在Petri网(N,M)中所有从标识M0可达的标识集合,可表示为R(N,M0)或个简化为R(M0)。从M0出发的所有可能发生序列的集合,可表示为L(N,M0)或简化为L(M0)。 这样,Petri网的可达性问题就转换为对于Petri网(N,M)和给定标识M0,寻找是存在M0 R

20、(M0) 可达性是研究任何系统动态特性而与基础,-49-,特性分析-有界性,对Petri网(N,M),若存在一个非负整数K,使得M0的任何一个可达标识的每个位置中的标记数都不超过K,即对每个标识MR(M0)和每个位置p,M (p) K 均成立,则称Petri网(N,M0)为K有界,或简称有界 若Petri网(N,M0)为1有界,则称此Petri网为安全的。这种网的每一个位置要么有一个标记,要么没有标记 通常用Petri网中的位置表示实际系统中存储数据的缓冲区和寄存器。通过分析网的有界性或安全性,就可以考察实际系统中缓冲区或寄存器是否会溢出,-50-,特性分析-活性,一个Petri网(N,M)被

21、称为活的或称M0是网N的一个活标识,仅当从M0可达的任一标识出发都可以通过执行某一转移序列而最终发生任一转移。这意味着,无论选择什么样的发生序列,一个活的Petri网都可以保证无死锁操作。活性是许多系统的理想特性。但这是不现实现的,也是不必要的 对于Petri网(N,M0)中的一个转移t,实际上可能属于以下情况: L0级活(死的):仅当t在L(M0)中任何发生序列中都无法发生 L1级活(可能能发生):仅当t 在L(M0)中的一些发生序列中至少可发生一次 L2级活:已知任一正整数k,仅当t 在L(M0)中的一些发生序列至少可发生k 次 L3级活:仅当t 在L(M0)中的一些发生序列中可以无限制的

22、发生 L4级活(活的):仅当t 在R(M0)中的每个标识是L1活的,-51-,特性分析-可逆性,一个Petri网(N,M0)称为可逆的,仅当对R (M0)中每个标识M,M0都是从M可达的。因此,一个可逆网可以返回到初始标识或初始状态。在很多名小应用中只要求系统回到某个特定状态而无需回到初始状声在态我们称这个特定状态为主(home)状态即对于R(M0)的每个标识M,主状态M 都是可达的 有界性、活性和可逆性是三种相互独立的特性,-52-,特性分析-可覆盖性,一个Petri网(N,M0)中一个标识M称做可覆盖的,仅当在R (M0)中存在一个标识M,使得对网中的每个位置M(p) M(p)成立 可覆盖

23、性与L1活(潜在的可发生性)紧密相关。设M是转移t发生所必需的最小标识。那么,当且仅当M是不可覆盖的,t是死的(非L1活)。也就是说,t是L1活,当且仅当M是可覆盖的,-53-,特性分析-持久性,一个Petri网(N,M0)称为持久的,仅当对于任意两个可发生转移,其中一个转移的发生不会使另一个转移不发生。就是说,持久网中的一个转移一旦可发生,将保持这种可发生性直至它发生为止 所有位置都只有一条输入孤和一条输出弧的Petri网(标识图)具有持久性,-54-,特性分析-同步距离,同步距离是条件/事件系统中两个 事件间相互独立程度紧密相关的 一种量度。我们用 来定义Petri网(N,M0)中两个转移

24、 t1 和t2 间的同步距离。其中 是起始于R (M0) 中的任何标识M 的一个发生序列,(t i )是转移 t i ( I = 1,2, )在 中发生的次数。 右图们仍所示Petri网中 d12=1,d34=1,d13= 同步有不同的形式(见例1例5),-55-,同步形式(1),它们共同执行一个任务,只有p1、p2中的标记同时到达时才能同步,-56-,同步形式(2),这是一个顺序系统,t1, t2为同步。但它们交替发生,t1与t2的关系为11,-57-,同步形式(3),这是一个并发系统,t1、t2发生的关系也为11。但它们不是交替发生,而可同时发生,也可一先一后发生,-58-,同步形式(4)

25、,本例中,t2不能先发生,只有t1可以发生。这也就是说,只有t1发生后,t2才能发生。这时,仍只有t1能够发生。即t1第二次发生后,t2才能发生。由此可见t1与t2也为顺序关系,但它们的关系为21,-59-,同步形式(5),本例中,t1与t2的关系为1或1,这就等于无同步可言,-60-,同步距离刻画事件间的同步关系,d12= 两组事件不同步,即异步 d12 两组事件以d12为距离相互同步 d12=0 两组事件在时间和空间上一起发生,网论中将它们当做一个事件 d12=1 两组事件必须交替发生,-61-,特性分析-公平性,两种基本公平性 有界公平性 对于两个转移,若不发生其中一个转移另一个转移可以

26、发生的最大次数是有界的,则称两个转移为有界-公平(或-公平)关系。若Petri网(N,M0)中每对转移都是-公平关系,则外该网为-公平网 无条件(全局)公平性 对于一个发生序列 ,若它为有限的或网中每个转移在中无限次出现,则称 为无条件(全局)公平的。 若从R(M0)中某个M开始的每个发生序列 都是无条公平的,则称Petri网(N,M0)为无条件公平网 两种类型公平性之间的关系 每个-公平网都是无条件公平网每个有界的无条件公平网都是-公平网,-62-,Petri网的特性分析方法,分层或化简 可覆盖性(可达性)树 不变量、关联矩阵和状态方程,-63-,Petri网的分层,Petri网分层的方法

27、自顶向下(一个子网替代一个结点) 自底向上(一个结点替代一个子网) 结点的选择 一般以转移t为结点,也可以位置p为结点 子网结构的限制 这是由于Petri网的异步并发性质决定的 解决的方法有:基于基本网和高级网的,有基于网的静态结构和动态行为的,也有基于形式化和非形式化的,还有基于网的静态结构的图论观点的,-64-,示例:Petri网的分层概念,与DFD分层相似。Petri网分层时,以作为分层的结点。不仅要保证父子层的I/O一致,还要保证它们的性质不变(因为Petri网主要用于并发系统的特性分析),-65-,示例:基于网的静态结构的图论观点,图中p1和p2分别为子网G的输入门和输出门。t1和t

28、2则分别分子网G”的输入门和输出门。G是一个位置子网,G”是一个转移子网。同时,它们的输入度(输入孤的数目)和输出度(输出弧的数目)均为1。有了这些概念就可以定义出如下化简子网的条件: 1,构成一条只有一个输 入门和一个输出门的直接路 经 2,输入门的输入度和输 出门的输出度分别为1 只有这样,才能保证原网 的特性(如活性、有界性等) 不变,-66-,Petri网的化简,与分层一样,是一种处理复杂问题的方法 化简的基本原则 在保持所有要求的性质不变的情况下,将多个不同位置或转移抽象为单个位置和转移 化简的方法 折叠(将结点多的基本网转换为结点少的高级网) 删减(将冗余或等价例位置或转移删除或合

29、并),-67-,Petri网的化简:折叠-着色网,这种方法是用颜色把标记分开 示例,-68-,Petri网的化简:折叠-谓词/转移网,这种方法与着色网不同,它用字符串来表示标记。然后,把转移与谓词(刻画标记的性质)联系起来,用来控制转移是否可发生 示例,-69-,高级网到基本网,高级网也可以展开为基本网 示例,-70-,Petri网的化简:删减,设(N,M)和(N,M)分别为化简前后的网,运用以下化简规则,当且仅当(N,M)是活的、安全的和有界的,则(N,M)是活的、安全的和有界的 串行位置的合并 串行转移的合并 并行位置的合并 并行转移的合并 自循环位置的消除 自循环转移的消除,-71-,串

30、行位置和转移的合并,-72-,并行位置和转移的合并,-73-,自循环位置和转移的消除,-74-,删减的示例,从图(a)发生t2,移去p1中标记,合并t1和t2为t12,合并t3和t4为t34,从而得出图(b)所示的Petri网。从图(b)中消去自循环转移t12和自循环位置p3,又可得以得出图(c )所示的Petri网。所有这三个网都是有界 的,非活的和安全 的,并且都是不可 逆的,-75-,可覆盖性(可达性)树,可覆盖性或可达性树用标识树来实现 标识树的实现 利用一个给定的Petri网(N,M0),从M0开始可以得数量与可发生转移一样多的许多“新的”标识。从各个新的标识可以再到达更多的标识。可

31、用标识树表示以上过程,以初始标识M0作树根,可由M0到达的标识作树的后继结点。每条连接结点的弧表示一个转移的发生,它将一个标识变换到另一个标识 标识树中的特殊符号 如果Petri网无界,则所构造的标识树将生长为无限。如果Petri网有界,所构造制标识树也可能为无限。另为了保持标识树的有限,我们引入一个特殊符号,可以把它想像为“无限”。 具有这样的性质: 对每个整数n: n, n= , ,-76-,可覆盖性(可达性)树的构造过程,1. 把初始标识M0当作根,并加上“新的”标志; 2. 当具有“新的”标志的标识存在时,重复以下步骤: (1)选择一个“新的”标识M; (2)如果M与从根到M 路径上的

32、一个标识相同,则对M 加上“老的” 标志,然后转向另一个“新的”标识; (3)如果M 中没有转移可以启动,对M 加上“死的”标志;为 (4)当M 中存在有效的转移时,对M 的每个转移t 做以下各步: a,从M 发生t 的结果获得标识M b,若M(p)= ,则M(p)= c,在从根到M 的路径上,如果存在一个标识M”,使得每个位置p 存在 M(p) M(p),并且M M,即M” 是可覆盖的。那么,对其中满足 M(p)M(p) 的每个位置p,用重置M(p) d. 引入M 作为树的一个结点,从M 向M 画用t 标注的弧,并对M 加上 “新的”标志。,-77-,从Petri网获得可覆盖性树,-78-,

33、使用可覆盖性树可研究Petri网的特性(1),对于一个Petri网(N, M0),且因此R(M0)是通过使用可覆盖性树可以研究以下特性 一个网(N, M0)是有界的,且因此R(M0)是有限的,当且仅当不会出现在可覆盖性树中的任一结点标注中 一个网(N, M0)是安全的,当且仅当只有“0”和“1”出现在可覆盖性树的结点标注中 一个转移t 是死的,当且仅当t 不出现在可覆盖性树的任一弧的标注中 如果M从M0可达,则存在一个标注M的结点,使得M M,-79-,使用可覆盖性树可研究Petri网的特性(2),对于一个有界的Petri网,其可覆盖性树被称为可达性树。这是因为它包括所有可能到达的标识。在这种

34、情况下,前面计讨论的所有行为特性的分析问题都可以通过可达性树来解决,这是一种穷举法 但在通常情况下,由于使用符号会使一些信息丢失,所以可达性和活性问题不可能单单利用可覆盖性树方法来解决。我们可看下页所示的两个不同的Petri网,它们有相同的可覆盖性树。但其中一个是活的Petri网,而另一个不是活的,因为该网在发生t1、t2和t3以后再也没有可发生的转移,-80-,使用可覆盖性树可研究Petri网的特性(3),两个不同的Petri网 一个活的Petri网 一个不活的Petri网,-81-,使用可覆盖性树可研究Petri网的特性(4),相同的可覆盖性树,-82-,使用可覆盖性树可研究Petri网的

35、特性(5),不同的可达状态 一个活的Petri网 一个不活的Petri网,-83-,不变量、关联矩阵和状态方程,这一部分介绍的是完全用代数计算来对网系统进行分析。 前边介绍的可达集都是从网的整体行为来刻画的。这里讲不变量,整体中有许多不变量,这是局部行为。 不变量用关联矩阵定义,它给出了系统的结构。 根据关联矩阵与网存在的一一对应关系推出状态方程。 最后就可用关联矩阵和状态方程计算出网的不变量和网的各种特性。,-84-,不变量(invariant),网系统中有S-不变量和T-不变量 如果网系统中有一些位置,其中包含的资源(标记)的总和在任何可达标识情况下均为常数,即系统不论发生什么事件,这些位

36、置中的标记总数不变,则这些位置就是系统的一个S-不变量。也就是说,S-不变量代表着网系统中若干个资源的流动范围 如果网系统中有一些转移,它们的发生会使它们的标识恢复到它们的开始状态,则这些转移就是系统的一个T-不变量,-85-,不变量-示例1,S-不变量和T-不变量一般采用向量表示,即以位置元素为序标的列向量表示S -不变量,以转移元素为序标的列向量表示T-不变量 本网系统的不变量为: S-不变量 T-不变量,-86-,不变量-示例2,本网系统的不变量:,-87-,不变量-示例3,本网系统的不变量:,-88-,关联矩阵(Incidence Matrix)( 1),正如网系统的标识可以表示为一个

37、向量一样,网结构也可以用一个矩阵来表示。 设=(N,M0),其中N=(P,T;F)是一个纯网,其中P=p1, p2, pm,T=t1,t2,tn 用S-元素作为序标的列向量V:PZ 称为的S-向量,Z为正负数集合。其中,Z=2, 1,0,1,2, 为正负数集合 用T-元素作为序标的列向量U: TZ 称为的T-向量 用PT作为序标的矩阵C: PTZ 称为的关联矩阵 其关联矩阵元素C (pi,tj )=W (tj,pi) W (pi,tj ),-89-,关联矩阵(2),C (pi,tj )=W (tj,pi) W (pi,tj )也可写成: Cijmn=Cijmn Cijmn 其中 Cij就是从转

38、移j到它的输出位置I的弧的权, Cij是抗持转移的输入伍卜位置I到转移j的弧的权。从转移规则很容易看出, Cij、 Cij和Cij 分别表示当转移j一旦发生,位置i中标记取走、增加和改变的数量。,-90-,关联矩阵(3),关联矩阵一般表示形式 其中Cij表一下示取走、增加后产生的变化数。此关联矩阵给出了系统的结构,-91-,状态方程,如果N=(P,T;F)是纯网,则C与N存在一一对应关系。在此,我们用m维列向量来表示标识M,即M=M(p1),M(p2), ,M(pm)T。这样,Mtj的充分必要条件为: i1,2, m:CijM (i) 或写成: C*j M 其中C*j表示矩阵Cij 的第j列。

39、 如果M1tj M2,则有M2=M1+ C*j。若M0 M,就可以推出状态方程为: M= M0+CU 其中CU是矩阵乘法,是的转移序列,U是的T-向量表示,它以tj为序标的分量值为tj在中出现的次数,即U(tj)=#(tj/ ),M0是的初始标识的S-向量表示,由导出的可达标识M也表示为S-向量形式。,-92-,用关联矩阵和状态方程求不变量,设I是的S-不变量,M M0 ,则 ITM=ITM0 设是从M0到M的转移序列:M0 M,于是 M0+CT U=M, 其中U是对应于的T-向量,对所有tj T,U(tj)是tj在 中出现的次数。两边同时乘以IT,则得 IT M0一+IT CT U=IT M

40、,-93-,状态方程在可达性分析中的应用(1),状态方程M = M0+CT U为部分解决可达性问题提供了一个依据。若Md 从 M0可达则方程CT U = Md M0 =M必然存在一个非负整数解Ux,该解即为发生的计数向量。若无这样的解,Md 就不继从M0到达。 示例1,-94-,状态方程在可达性分析中的应用(2),示例1(续) 在所示的Petri网中: 在状态M0下转移t3是可发生的。设M1是发生t3所得的标识,则有,-95-,状态方程在可达性分析中的应用(3),示例1(续) 发生序列=t3 t2 t3 t2 t1表示成发生计数向量(1,2,2),发生后产生的新标识为,-96-,状态方程在可达

41、性分析中的应用(4),示例1(续) 考察标识 ,它可以从标识M0到达方程为 有一个解U=(0,4,5),它对应于发生序列=t3 t2 t3 t2 t3 t2 t3 t2 t3,-97-,状态方程在可达性分析中的应用(5),再考察后标识 ,因方程 无解,所以标识 为不可达标识,-98-,状态方程在可达性分析中的应用(6),注意,状态方程有解只是可达性的必要条件,而不是充分条件。这是由于缺少M 初始标识信息导致的 示例2 考察所示的Petri网,-99-,状态方程在可达性分析中的应用(7),示例2(续) 在所示的Petri网中 方程,-100-,状态方程在可达性分析中的应用(8),示例2(续) 有

42、一个解U = 。这个解对应的两个可能发生序列为t1 t2或t2 t1,然而这两个序列都不是可发生序列。因为在M0下,t1、t2都不可能发生。这里 若取初始标识为 则为可达的,且对应于发生计数向量 的发生序列为t1t2,-101-,关联矩阵和状态方程在其他特性方面的应用(1),结构有界性 N=(P,T;F)称为结构有界,是指对任何初始标识M0,(N,M0)都是有界的。可以证明,网N 结构有界的充分必要条件是存在m 维正整数向量V,使得CTV0 守恒性 如果存在P上的一个正整数函数V,使得对任何初始标识M0和任何MR (M0),M (i )V (i )为一固定值,则称N为守恒的。可以证明,网N守恒

43、的充分必要条件是存在m 维正整数向量V,使得CT V=0 可重复性 如果在存在初始标识M0,在(N,M0)中存在无限转移序列,使得M0,而且每个转移tj 都在 中出现无限多次,则称网N为可重复的。可以证明,网N可充分必要条件是存在n 维正整数向量U,使得C U0,-102-,关联矩阵和状态方程在其他特性方面的应用(2),相容性 如果存在初始标识 M0,在(N,M0)中存在无限转移序列,使得M0 M0,而且tj T,# (tj /) 1,则称网N为可相容的。可以证明,网N 为相容的充分必要条件是存在n 维正整数向量U,使得C U = 0 结构公平性 如果对任何初始标识M0,在(N,M0)中都是公

44、平网,则称网N为公平网。 可以证明,网N 为公平网的充分必要条件是对任意n 维非负整数向量U:C U 0 i 1,2, , m:U (i) 0,而且若有U1和U2 满足C U 1 0 和 C U 2 0 ,则U 1和U 2 线性相关,-103-,关联矩阵和状态方程在其他特性方面的应用(3),示例 本例所示的网(N,M0),它的位置集S和转移集T各有4个元素,流关系如图所示,初始标识M0=1,0,0,0。对这样的网(N,M0),可以写出它的关联矩阵和状态方程,-104-,关联矩阵和状态方程在其他特性方面的应用(4),由于M0C*2,所以t2可以发生。设M0t2M1,则 如没=t2t1t2t1t2

45、t4在M0可以发生,记M0M2,则可计算出M2为,-105-,关联矩阵和状态方程在其他特性方面的应用(5),本例容易证明,存在U1= 使得CU1=0。所以网N是相容的,也是可重复 的。但不存在四维正整数向量V,使得CTV0。所以网N不是结构有界的 对于任意非负整数kV=k 都满足CTV=0。何所以k 是N 的一个S-不 变量,从而S1,S2,S4是N 的S-不变量的支集。 同理,N 的T-不变量额广都有k 的形式,也即转移集T本身是N 的T-不变量的支集 由于存在U2= ,使得CU2= ,而U2中含有零分量。所以N不是公平,-106-,改进Petri网及其应用,什么是改进Petri网 改进Pe

46、tri网指的是谓词/转移网和着色网。它们由基本网改进而来,故称它们为改进Petri网。有的称它们为变形网,还有的称它们为高级网 既然有了上面讨论的基本网,为什么还要高级网 这是因为在实际应用中,一个稍复杂的网系统就会使用大量的位置和转移,由此引起状态组合爆炸问题,使Petri网难以理解和分析。有人甚至认为在状态(可达集)组合爆炸这一基本问题未获解决或有可能避免之前,Petri网建模不可能出现实质性的成功或突破。所以还要介绍高级网。 高级网系统如何构造 高级网系统如何构造,一般都从应用的问题的P/T网系统模型着手,经折叠而成。所以,我们就应该先弄清什么是P/T网系统的折叠,然后介绍折叠的高级网系

47、统的定义 什么是折叠 折叠就是采用抽象的方法,把具有同类逻辑功能制的位置和转移进行合并,这样就可以大大减少位置和转移的数量,将结点多的P/T网系统转换为结点较少的高级网系统,-107-,谓词/转移网,谓词/转移网(Predicate/Transition nets, Pr/T网) Pr/T网的转移发生条件和引起的标识变化是通过刻画标记性质的谓词来解释的 示例:一个机械制造车间零件加工的简化Pr/T网系统模型,-108-,一个机械制造车间零件加工的简化Pr/T网系统模型(1),1,问题描述 有一名工人分别在机床甲和机床乙上加工零件。先加工完的机床要等待另一台机床加工完后,零件经装配才能卸下。然后

48、,机床转入空闲,再进入就绪。以上加工过程重复进行 为简化问题,这里只考虑工人和机床的关系。其他如原材料来源、成品的去处,以及辅助工具(刀、量等)等一概不考虑,-109-,一个机械制造车间零件加工的简化Pr/T网系统模型(2),2,P/T网系统模型,-110-,一个机械制造车间零件加工的简化Pr/T网系统模型(3),3,先分析位置 从上可知:本系统中有3 个个体:工人、机床甲作和机床乙,用w、a、b来表示 这3 个个体可能处于4 种状态:就绪(ready)、工作(working)、等待(waiting)和休息(resting) 工作必须是w和a或w和b的结合,为了强调结合用joint(结合)表示

49、working 如果用P-元素表示4个状态,用w、a、b三个个体名代替没有个性的标记。就可把逻辑功能相同的位置(状态)折叠在一起 这样位置由10个减少为4个,-111-,一个机械制造车间零件加工的简化Pr/T网系统模型(4),逻辑功能相同的位置折叠在一起的图形表示,-112-,一个机械制造车间零件加工的简化Pr/T网系统模型(5),在位置折叠的图中可见 它保留了P/T网系统中的全部有向孤和所有转移。有向张上旅弧上标注了孤上流动的个体或由个体结合而成的偶如w,a或w,b P-元素(位置)已不是原P/T网系统中的位置,而是其中个体当前的状态,即谓词。谓词中的标识也不是非负整数,而是由个体组成的集合

50、。如P1中初始标识有3个个体,表明w、a、b都处于就绪状态。P2、P3和P4在初始标识下,均无个体,为空集。由此可见,引进谓词后,减少了P (位置)的个数,-113-,一个机械制造车间零件加工的简化Pr/T网系统模型(4),4,再分析转移 很明显,由上图可见:转移也可分为4类:结合(joint)(开始工作)=t1,t2、完成(finish)(工作完成)=t3,t4、装配(assemble)=t5和准备(to-ready)=t6,t7,t8 由上图还可见:同类转移有相同的前集和后集,t1与t2、t3与t4,以及t6、t7和t8之间的区别在于参与转移的个体不同。如果我们用变量x来代替个体名,则可把

51、同类转移也合并为一个。这就可以得到合并转移后的网系统,-114-,一个机械制造车间零件加工的简化Pr/T网系统模型(5),合并转移后得到的网系统,-115-,一个机械制造车间零件加工的简化Pr/T网系统模型(6),在转移折叠的图中可见 把P、T 两个元素间的多条有向弧合并为一条,弧上标注也用“+”号连在一起。如P1与t1、t2之间的两条弧合并为一条后,弧上记为w+x,x表示P1中的任何一个个体。为统一符号,w,a和w,b可改写为w,x。用尖括号及“+”号连在一起的表达式为符号和 必须指出,w+x是两个独立的个体,w,x是两个结合在一起的个体 新转移joint、finish、assemble和t

52、o-ready分别代表系统中的同一类转移 当从P1到joint的弧上标注w+x中的变量x取个体a为值时,转移joint发生就是原系统中t1的发生。当x以b为值时,joint发生不是t1,而是t2。但x不能以w为值 图中只使用了一个变量名x,但x并非表示同一个变量。事实上,只有同一个转移的所有I/O弧上的变量才是同一个变量,它必须取同一个个体为值。由此可见,引进变量后减少了T-元素的个数,-116-,一个机械制造车间零件加工的简化Pr/T网系统模型(7),5,Pr/T网系统的转移规则 Pr/T网系统的标识为系统中每个谓词指明了其外延。在转移的折叠图中P1的外延为|a,b,w |,写成符号和为+。

53、而P2、P3和P4的外延均为空集合。转移joint前后的变量x可以分别以a和b值发生,发生的两次转移分别记为joint(xa)和joint(xa),而x a 和xb称为转移joint的可行替换,即以a替换x和以b替换x。这肘转移才有发生权和发生权的后继。对joint而言,x w不是可行替换,joint(x w )在初始标下没有发生权。所以Pr/T网系统不能离开变量替换来讨论 joint (xa)发生伪一的后果是化从P1中拿走个体a和w,在P2中加上a和w的结合,这些都是由joint的I/O弧上的标注和替换xa计算出来的。joint (xa)发生后的后继M1为M1(P1)=,M1(P2)=|,M

54、1(P3)=M1(P4)=null,即空符号和 按上述规则,可以给出转移折叠图的Pr/T网系统中一些可能替换及相应的谓词外延的变化如下页列表所示,-117-,一个机械制造车间零件加工的简化Pr/T网系统模型(8),Pr/T网系统的转移规则(续) 谓词外延的变化 表中谓词外延以集合形式给出以便比较集合的形式与符号和的对 应关系,-118-,一个机械制造车间零件加工的简化Pr/T网系统模型(9),6,Pr/T网系统的定义 =(P,T;F,D,V,A,M0) 其中 (P,T;F)为有向网,即的基网 D 为非空有限集,即的个体集(标记的分类) V 为D上的变量集 A 为有向集F上的可变谓词集(这些谓词

55、是以V 的元素为变元的逻辑式或代数式) M0 为状态的初始标识 说明 定义中没有明确给出的两点要求是:M0 必须是D 在谓词集P上的一个分布,而每个转移tT 必须是个体守恒的。转移t 的个体字恒表现在,即出现在它的输入弧上的个体必须也出现在它的输出弧上。反之亦然。出现的形式可以不同,-119-,一个机械制造车间零件加工的简化Pr/T网系统模型(10),7,Pr/T网系统的行为 与P/T网系统相同点 谓词/转移网和着色网实质上都是P/T网系统为与折叠和扩充行为上自然类似顺序并发和冲突等基本现象都可以得到严格的描述。所以,分析P/T网系统行为的方法都可以用来分析Pr/T网系统和着色网系统 与P/T

56、网系统不同点 因为Pr/T网系统中的标识都是一种个体的分布,而且每个转移都是个体守恒的,所以Pr/T网中不会有冲突 另外,谓词只是个体状态的一种描述,所以P(位置)元素应该没有容量限制。因而一般不会发生碰撞 也可以使用P/T网系统构造可达树的方法,对Pr/T网系统进行分析。但Pr/T网系统的可达树的结点标识中不会出现“”。因为Pr/T网系统中每个标识都是个体集中的一种个体分布,而有限个个体在有限个谓词中的分布一共只有有限种,所以Pr/T网系统的可达树也是有限的,-120-,着色网(colored nets),着色网通过颜色区分标记,通过增加位置的颜色集和转移出现的颜色集,以及转移的I/O函数来

57、刻画解释 1,定义 =(P,T;F,C,I-,I+,M0) 其中 (P,T;F)分广为有向网,即的基网 C为颜色集合,并有 对p P,C (p)是位置p上所有可能标记颜色非空有限集合 对t T,C (t)是转移t 上所有可能出现的颜色非空有限集合 I-和I+分别为PT 和TP上的负函数和正函数 p P, t T I-(p,t) 0 I+(t,p) 0 t T, p P I-(p,t) 0 I+(t,p) 0 M0为的初始标识,-121-,2,着色网系统定义中的符号含义(1),这里仍使用Pr/T网系统的示例说明 (1)C(颜色集合) 系统有3个个体(a,b,w)和4种状态(就绪、工作、等待和休息

58、),这样就可以给出位置p上的所有可能的标记颜色集合 C(p1)=, C(p2)=a,b C(p3)=a,b,w 同样系统中的转移也有4类(结合、完成、装配和推产准备),这样也就可以给出所有可以出现的颜色集合 C(joint)=, C(finish)=, C(assemble)= C(to-ready)=,-122-,2,着色网系统定义中的符号含义(2),这里仍使用Pr/T网系统的示例说明(续) (2) I-和I+(PT和TP上的负函数和正函数) 只有上面颜色说明还不够,还应当说明转移发生时其I/O位置中标记的变化 I-(joint,p1,)=1 I-(joint,p1,)=1 I+(joint ,p2,)=1 I+(joint,p2,)=1 I- (finish,p2,)=1 I -(finish,p2,)=1 I+(finish,p3,a)=1 I+(finish,p4,w )=1 I+(finish,p3,b)=1 I+(finish,p4,w )=1 I-(assemble,p3,)=1 I+(assemble,p4,)=1 I-(to-ready,p4,)=1 I+(to-eady,p1,)=1 这样,着色网系统表示的语义就非常清楚了 从中还可发现a、b也为

温馨提示

  • 1. 本站所有资源如无特殊说明,都需要本地电脑安装OFFICE2007和PDF阅读器。图纸软件为CAD,CAXA,PROE,UG,SolidWorks等.压缩文件请下载最新的WinRAR软件解压。
  • 2. 本站的文档不包含任何第三方提供的附件图纸等,如果需要附件,请联系上传者。文件的所有权益归上传用户所有。
  • 3. 本站RAR压缩包中若带图纸,网页内容里面会有图纸预览,若没有图纸预览就没有图纸。
  • 4. 未经权益所有人同意不得将文件中的内容挪作商业或盈利用途。
  • 5. 人人文库网仅提供信息存储空间,仅对用户上传内容的表现方式做保护处理,对用户上传分享的文档内容本身不做任何修改或编辑,并不能对任何下载内容负责。
  • 6. 下载文件中如有侵权或不适当内容,请与我们联系,我们立即纠正。
  • 7. 本站不保证下载资源的准确性、安全性和完整性, 同时也不承担用户因使用这些下载资源对自己和他人造成任何形式的伤害或损失。

评论

0/150

提交评论