《形式化开发方法网.ppt》由会员分享，可在线阅读，更多相关《形式化开发方法网.ppt（141页珍藏版）》请在三一办公上搜索。
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双重类兼有操作类和描述类两者的特点扩展状态机（ESM）、实时时态逻辑（RTTL）,-
4、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网的基本原理-静态结构Petri网的基本原理-动态特征建模实例特性分析Petri网的特性分析方法改进Petri网及其应
7、用时间网和随机网从Petri网到程序结构的转换,-15-,示例：四季系统,一年有四季，四季气候的变化,该系统可以由图形表示,-16-,系统的Petri网图形表示,-17-,系统的Petri网数学表示,=（P，T；F，M0）P=p1,p2,p3,p4T=t1,t2,t3,t4F=（p1,t1）,（t1,p2）,（p2,t2）,（t2,p3）,（p3,t3）,（t3,p4）,（p4,t4）,（t4,p1）M0=（0,0,0,1）,-18-,Petri网描述系统的特点,从四季系统中，可以看出这种利用事物的因果关系对系统进行网状结构的描述，有以下特点自然没有任何不必要的人为控制，完全反映了现实世界的真
8、实情况局部确定原理因为事件或转移的发生和结果都由局部状态决定既有系统静态结构，又有动态行为方面的信息既有图形工具，又有数学工具图形工具和数学工具完全等价图形工具直观、形象、易懂、易学；数学工具严谨，既便于计算，又便于验证,-19-,Petri网的基本原理：静态结构,任何系统都有两类元素组成：表示状态的元素和表示状态变化的元素Petri网位置（place）：状态转移（transition）：改变状态两者之间的依赖关系用弧（箭头）表示,-20-,Petri网的基本成分（1）,-21-,Petri网的基本成分（2）,其中：P=（p1,p2,pm）是N的有穷位置集合,T=（t1,t2,tn）是N的有穷
9、转移集合,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两者间的流关系F是从它们构造出来的。所以在P、T之后的F用分号“；”隔开来PT 说明网中至少要有一个元素,PT=说明P和T为两类不同的元素,两者不能有交F（PT）（TP）说明一个P元素代表一个资源,其流动由F关系
10、规定。所以,转移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;F1）和N2=（P2,T2;F2）中，如果,且,则称N1是N2的子网。,-24-,纯网,在N=（P,T；F）中,如果对似有xPT,都有*x x*=,则称N为纯网（pure net）纯网中无公共前后集（环）,-25-,简单网,如果对所有x,
11、yPT,都有（*x=*y）（x*=y*）x=y,则称N为简单网（simple net）简单网中无相同的前后集,-26-,Petri网的基本原理：动态特征（1）,Petri网作为系统的建模工具,除具有上述描述的静态结构外,还应包括位置的容量和转移发生对位置容量的影响信息。有限容量可用大于零的整数表示,转移发生对位置中标记数的影响用孤上的整数表示。于是,具有动态特征的Petri网可表示为六元组：,-27-,Petri网的基本原理：动态特征（2）,Petri网的六元组：其中：（P,T；F）含义同前 K：PN 是位置上的容量函数,N=0,1,2,3,若K（p）=,表示位置中的容量为无穷 W：F N是孤
12、集合上的孤函数 M：P N0是Petri网的标识（marking）。M0为初始标识,N0=0,1,2,3,pP,必须满足M（p）K（p）在Petri网的图形表示中,M（p）不是用数字,而是用实圆点表示。每个实圆点为一个标记,同一个位置中的诸多标记代表同一类完全等价的个体。弧（x,y）上的W值标注在孤（x,y）上,-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 下可
13、发生,记为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）W（t,p）当p*t t*=M（p）当pt*t,-29-,转移发生规则（2）,注意一个没有任何输入位置的转移叫源转移,一个源转移的可发生是无条件的。一个源转移的发生只会产生标记,而不消耗任何标记一个没有任何输出位置的转移叫潭转移,一个潭转移的发生将消耗标记,而不产生任何标记,-30-,示例：转移发生规则,以本例来说明网论中的转移发生规则，以及网论
14、中的冲突（conflict）、并发（concurrent）和碰撞（contact）现象有时，一个Petri网中同时存在并发和冲突，而且并发的发生会引起冲突的消失或出现。网论中称这种现象为混惑（confusion）,-31-,并发和冲突概念的完整描述,并发设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 为基本网（elem
15、entary net,EN）系统这种网系统位置p 中，只有有标记和无标记两种状态。习惯上把这种网称为条件/转移网系统K，W1 为P/T（place/transition）网K和W为任意函效 为P/T系统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-
16、,Petri网转移发生规则的简化,对Petri网简化的原因是为了对Petri网进行理论上研究的方便通过上面讨论可以看出，对于简单的Petri网，由于K和W已无任何限制作用。所以，一般把这种Petri网系统记为：=（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
17、（p）其它,-34-,建模实例：有限状态机,-35-,建模实例：并行活动,-36-,建模实例：数据流计算,-37-,建模实例：通信协议,-38-,建模实例：同步控制,-39-,建模实例：生产者/消费者系统（1）,-40-,建模实例：生产者/消费者系统（2）,抑制弧,-41-,建模实例：形式语言,-42-,建模实例：机械加工（1）,-43-,建模实例：机械加工（2）,-44-,建模实例：机械加工（3）,-45-,建模实例：机械加工（4）,-46-,建模实例：机械加工（5）,-47-,特性分析,Pretri网的特性主要包括可达性（Reachability）有界性（Boundedness）活性（Li
18、veness）可逆性（Reversibility）可覆盖性（Coverability）持久性（Persistence）同步距离（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（M
19、0）。这样,Petri网的可达性问题就转换为对于Petri网（N,M）和给定标识M0,寻找是存在M0 R（M0）可达性是研究任何系统动态特性而与基础,-49-,特性分析-有界性,对Petri网（N,M），若存在一个非负整数K，使得M0的任何一个可达标识的每个位置中的标记数都不超过K，即对每个标识MR（M0）和每个位置p,M（p）K 均成立，则称Petri网（N,M0）为K有界，或简称有界若Petri网（N,M0）为1有界，则称此Petri网为安全的。这种网的每一个位置要么有一个标记，要么没有标记通常用Petri网中的位置表示实际系统中存储数据的缓冲区和寄存器。通过分析网的有界性或安全性，就可以
20、考察实际系统中缓冲区或寄存器是否会溢出,-50-,特性分析-活性,一个Petri网（N,M）被称为活的或称M0是网N的一个活标识，仅当从M0可达的任一标识出发都可以通过执行某一转移序列而最终发生任一转移。这意味着，无论选择什么样的发生序列，一个活的Petri网都可以保证无死锁操作。活性是许多系统的理想特性。但这是不现实现的，也是不必要的对于Petri网（N，M0）中的一个转移t，实际上可能属于以下情况：L0级活（死的）：仅当t在L（M0）中任何发生序列中都无法发生L1级活（可能能发生）：仅当t 在L（M0）中的一些发生序列中至少可发生一次L2级活：已知任一正整数k，仅当t 在L（M0）中的一些
21、发生序列至少可发生k 次L3级活：仅当t 在L（M0）中的一些发生序列中可以无限制的发生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
22、（M0）中存在一个标识M，使得对网中的每个位置M（p）M（p）成立可覆盖性与L1活（潜在的可发生性）紧密相关。设M是转移t发生所必需的最小标识。那么，当且仅当M是不可覆盖的，t是死的（非L1活）。也就是说，t是L1活，当且仅当M是可覆盖的,-53-,特性分析-持久性,一个Petri网（N,M0）称为持久的，仅当对于任意两个可发生转移，其中一个转移的发生不会使另一个转移不发生。就是说，持久网中的一个转移一旦可发生，将保持这种可发生性直至它发生为止所有位置都只有一条输入孤和一条输出弧的Petri网（标识图）具有持久性,-54-,特性分析-同步距离,同步距离是条件/事件系统中两个 事件间相互独立程度
23、紧密相关的 一种量度。我们用 来定义Petri网（N,M0）中两个转移 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。但它们不是交替发生，而可同时
24、发生，也可一先一后发生,-58-,同步形式（4）,本例中，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-,特性分析-公平性,两种基本公平性有界公平性对于两个转移，若不
25、发生其中一个转移另一个转移可以发生的最大次数是有界的，则称两个转移为有界-公平（或-公平）关系。若Petri网（N,M0）中每对转移都是-公平关系，则外该网为-公平网无条件（全局）公平性对于一个发生序列，若它为有限的或网中每个转移在中无限次出现，则称 为无条件（全局）公平的。若从R（M0）中某个M开始的每个发生序列 都是无条公平的，则称Petri网（N,M0）为无条件公平网两种类型公平性之间的关系每个-公平网都是无条件公平网每个有界的无条件公平网都是-公平网,-62-,Petri网的特性分析方法,分层或化简可覆盖性（可达性）树不变量、关联矩阵和状态方程,-63-,Petri网的分层,Petri
26、网分层的方法自顶向下（一个子网替代一个结点）自底向上（一个结点替代一个子网）结点的选择一般以转移t为结点，也可以位置p为结点子网结构的限制这是由于Petri网的异步并发性质决定的解决的方法有：基于基本网和高级网的，有基于网的静态结构和动态行为的，也有基于形式化和非形式化的，还有基于网的静态结构的图论观点的,-64-,示例：Petri网的分层概念,与DFD分层相似。Petri网分层时，以作为分层的结点。不仅要保证父子层的I/O一致，还要保证它们的性质不变（因为Petri网主要用于并发系统的特性分析）,-65-,示例：基于网的静态结构的图论观点,图中p1和p2分别为子网G的输入门和输出门。t1和t
27、2则分别分子网G”的输入门和输出门。G是一个位置子网，G”是一个转移子网。同时，它们的输入度（输入孤的数目）和输出度（输出弧的数目）均为1。有了这些概念就可以定义出如下化简子网的条件：1，构成一条只有一个输 入门和一个输出门的直接路 经 2，输入门的输入度和输 出门的输出度分别为1 只有这样，才能保证原网 的特性（如活性、有界性等）不变,-66-,Petri网的化简,与分层一样，是一种处理复杂问题的方法化简的基本原则在保持所有要求的性质不变的情况下，将多个不同位置或转移抽象为单个位置和转移化简的方法折叠（将结点多的基本网转换为结点少的高级网）删减（将冗余或等价例位置或转移删除或合并）,-67-
28、,Petri网的化简：折叠-着色网,这种方法是用颜色把标记分开示例,-68-,Petri网的化简：折叠-谓词/转移网,这种方法与着色网不同，它用字符串来表示标记。然后，把转移与谓词（刻画标记的性质）联系起来，用来控制转移是否可发生示例,-69-,高级网到基本网,高级网也可以展开为基本网示例,-70-,Petri网的化简：删减,设（N,M）和（N,M）分别为化简前后的网，运用以下化简规则，当且仅当（N,M）是活的、安全的和有界的，则（N,M）是活的、安全的和有界的串行位置的合并串行转移的合并并行位置的合并并行转移的合并自循环位置的消除自循环转移的消除,-71-,串行位置和转移的合并,-72-,并
29、行位置和转移的合并,-73-,自循环位置和转移的消除,-74-,删减的示例,从图（a）发生t2,移去p1中标记,合并t1和t2为t12,合并t3和t4为t34,从而得出图（b）所示的Petri网。从图（b）中消去自循环转移t12和自循环位置p3,又可得以得出图（c）所示的Petri网。所有这三个网都是有界 的,非活的和安全 的,并且都是不可 逆的,-75-,可覆盖性（可达性）树,可覆盖性或可达性树用标识树来实现标识树的实现利用一个给定的Petri网（N,M0），从M0开始可以得数量与可发生转移一样多的许多“新的”标识。从各个新的标识可以再到达更多的标识。可用标识树表示以上过程，以初始标识M0作
30、树根，可由M0到达的标识作树的后继结点。每条连接结点的弧表示一个转移的发生，它将一个标识变换到另一个标识标识树中的特殊符号如果Petri网无界，则所构造的标识树将生长为无限。如果Petri网有界，所构造制标识树也可能为无限。另为了保持标识树的有限，我们引入一个特殊符号，可以把它想像为“无限”。具有这样的性质：对每个整数n：n，n=，,-76-,可覆盖性（可达性）树的构造过程,1.把初始标识M0当作根，并加上“新的”标志；2.当具有“新的”标志的标识存在时，重复以下步骤：（1）选择一个“新的”标识M；（2）如果M与从根到M 路径上的一个标识相同，则对M 加上“老的”标志，然后转向另一个“新的”标
31、识；（3）如果M 中没有转移可以启动，对M 加上“死的”标志；为（4）当M 中存在有效的转移时，对M 的每个转移t 做以下各步：a，从M 发生t 的结果获得标识Mb，若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-,使用可覆盖性树可研究Petri网的特性（1）,对于一个Petri网（N,M0），且因此R（
32、M0）是通过使用可覆盖性树可以研究以下特性一个网（N,M0）是有界的，且因此R（M0）是有限的，当且仅当不会出现在可覆盖性树中的任一结点标注中一个网（N,M0）是安全的，当且仅当只有“0”和“1”出现在可覆盖性树的结点标注中一个转移t 是死的，当且仅当t 不出现在可覆盖性树的任一弧的标注中如果M从M0可达，则存在一个标注M的结点，使得M M,-79-,使用可覆盖性树可研究Petri网的特性（2）,对于一个有界的Petri网，其可覆盖性树被称为可达性树。这是因为它包括所有可能到达的标识。在这种情况下，前面计讨论的所有行为特性的分析问题都可以通过可达性树来解决，这是一种穷举法但在通常情况下，由于使
33、用符号会使一些信息丢失，所以可达性和活性问题不可能单单利用可覆盖性树方法来解决。我们可看下页所示的两个不同的Petri网，它们有相同的可覆盖性树。但其中一个是活的Petri网，而另一个不是活的，因为该网在发生t1、t2和t3以后再也没有可发生的转移,-80-,使用可覆盖性树可研究Petri网的特性（3）,两个不同的Petri网一个活的Petri网 一个不活的Petri网,-81-,使用可覆盖性树可研究Petri网的特性（4）,相同的可覆盖性树,-82-,使用可覆盖性树可研究Petri网的特性（5）,不同的可达状态一个活的Petri网 一个不活的Petri网,-83-,不变量、关联矩阵和状态方程
34、,这一部分介绍的是完全用代数计算来对网系统进行分析。前边介绍的可达集都是从网的整体行为来刻画的。这里讲不变量，整体中有许多不变量，这是局部行为。不变量用关联矩阵定义，它给出了系统的结构。根据关联矩阵与网存在的一一对应关系推出状态方程。最后就可用关联矩阵和状态方程计算出网的不变量和网的各种特性。,-84-,不变量（invariant）,网系统中有S-不变量和T-不变量如果网系统中有一些位置，其中包含的资源（标记）的总和在任何可达标识情况下均为常数，即系统不论发生什么事件，这些位置中的标记总数不变，则这些位置就是系统的一个S-不变量。也就是说，S-不变量代表着网系统中若干个资源的流动范围如果网系统
35、中有一些转移，它们的发生会使它们的标识恢复到它们的开始状态，则这些转移就是系统的一个T-不变量,-85-,不变量-示例1,S-不变量和T-不变量一般采用向量表示，即以位置元素为序标的列向量表示S-不变量，以转移元素为序标的列向量表示T-不变量本网系统的不变量为：S-不变量 T-不变量,-86-,不变量-示例2,本网系统的不变量：,-87-,不变量-示例3,本网系统的不变量：,-88-,关联矩阵（Incidence Matrix）（1）,正如网系统的标识可以表示为一个向量一样，网结构也可以用一个矩阵来表示。设=（N,M0）,其中N=（P,T;F）是一个纯网，其中P=p1,p2,pm，T=t1,t
36、2,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就是从转移j到它的输出位置I的弧的权，Cij是抗持转移的输入伍卜位置I到转移j的弧的权。从转移规则很容易看出，Cij、Cij和Cij 分别表示当转移j一旦发生，位置i中标记取走、增加和改变的
37、数量。,-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列。如果M1tj M2，则有M2=M1+C*j。若M0 M，就可以推出状态方程为：M=M0+CU 其中CU是矩阵乘法，是的转移序列，U是的T-向量表示，它以tj为序标的分量值为tj在中出现的次数，即U（tj）
38、=#（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,-93-,状态方程在可达性分析中的应用（1）,状态方程M=M0+CT U为部分解决可达性问题提供了一个依据。若Md 从 M0可达则方程CT U=Md M0=M必然存在一个非负整数解Ux，该解即为发生的计数向量。若无这样
39、的解，Md 就不继从M0到达。示例1,-94-,状态方程在可达性分析中的应用（2）,示例1（续）在所示的Petri网中：在状态M0下转移t3是可发生的。设M1是发生t3所得的标识，则有,-95-,状态方程在可达性分析中的应用（3）,示例1（续）发生序列=t3 t2 t3 t2 t1表示成发生计数向量（1,2,2），发生后产生的新标识为,-96-,状态方程在可达性分析中的应用（4）,示例1（续）考察标识，它可以从标识M0到达方程为有一个解U=（0,4,5），它对应于发生序列=t3 t2 t3 t2 t3 t2 t3 t2 t3,-97-,状态方程在可达性分析中的应用（5）,再考察后标识，因方程无
40、解，所以标识 为不可达标识,-98-,状态方程在可达性分析中的应用（6）,注意，状态方程有解只是可达性的必要条件，而不是充分条件。这是由于缺少M 初始标识信息导致的示例2 考察所示的Petri网,-99-,状态方程在可达性分析中的应用（7）,示例2（续）在所示的Petri网中方程,-100-,状态方程在可达性分析中的应用（8）,示例2（续）有一个解U=。这个解对应的两个可能发生序列为t1 t2或t2 t1，然而这两个序列都不是可发生序列。因为在M0下，t1、t2都不可能发生。这里若取初始标识为则为可达的，且对应于发生计数向量 的发生序列为t1t2,-101-,关联矩阵和状态方程在其他特性方面的
41、应用（1）,结构有界性N=（P,T；F）称为结构有界，是指对任何初始标识M0，（N,M0）都是有界的。可以证明，网N 结构有界的充分必要条件是存在m 维正整数向量V，使得CTV0守恒性如果存在P上的一个正整数函数V，使得对任何初始标识M0和任何MR（M0），M（i）V（i）为一固定值，则称N为守恒的。可以证明，网N守恒的充分必要条件是存在m 维正整数向量V，使得CT V=0可重复性如果在存在初始标识M0，在（N,M0）中存在无限转移序列，使得M0，而且每个转移tj 都在 中出现无限多次，则称网N为可重复的。可以证明，网N可充分必要条件是存在n 维正整数向量U，使得C U0,-102-,关联矩阵
42、和状态方程在其他特性方面的应用（2）,相容性如果存在初始标识 M0，在（N,M0）中存在无限转移序列，使得M0 M0，而且tj T，#（tj/）1，则称网N为可相容的。可以证明，网N 为相容的充分必要条件是存在n 维正整数向量U，使得C U=0结构公平性如果对任何初始标识M0，在（N,M0）中都是公平网，则称网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,
43、M0），它的位置集S和转移集T各有4个元素，流关系如图所示，初始标识M0=1,0,0,0。对这样的网（N,M0），可以写出它的关联矩阵和状态方程,-104-,关联矩阵和状态方程在其他特性方面的应用（4）,由于M0C*2，所以t2可以发生。设M0t2M1，则如没=t2t1t2t1t2t4在M0可以发生，记M0M2，则可计算出M2为,-105-,关联矩阵和状态方程在其他特性方面的应用（5）,本例容易证明，存在U1=使得CU1=0。所以网N是相容的，也是可重复 的。但不存在四维正整数向量V，使得CTV0。所以网N不是结构有界的对于任意非负整数kV=k 都满足CTV=0。何所以k 是N 的一个S-不
44、变量，从而S1,S2,S4是N 的S-不变量的支集。同理，N 的T-不变量额广都有k 的形式，也即转移集T本身是N 的T-不变量的支集由于存在U2=，使得CU2=，而U2中含有零分量。所以N不是公平,-106-,改进Petri网及其应用,什么是改进Petri网改进Petri网指的是谓词/转移网和着色网。它们由基本网改进而来，故称它们为改进Petri网。有的称它们为变形网，还有的称它们为高级网既然有了上面讨论的基本网，为什么还要高级网这是因为在实际应用中，一个稍复杂的网系统就会使用大量的位置和转移，由此引起状态组合爆炸问题，使Petri网难以理解和分析。有人甚至认为在状态（可达集）组合爆炸这一基
45、本问题未获解决或有可能避免之前，Petri网建模不可能出现实质性的成功或突破。所以还要介绍高级网。高级网系统如何构造高级网系统如何构造，一般都从应用的问题的P/T网系统模型着手，经折叠而成。所以，我们就应该先弄清什么是P/T网系统的折叠，然后介绍折叠的高级网系统的定义 什么是折叠折叠就是采用抽象的方法，把具有同类逻辑功能制的位置和转移进行合并，这样就可以大大减少位置和转移的数量，将结点多的P/T网系统转换为结点较少的高级网系统,-107-,谓词/转移网,谓词/转移网（Predicate/Transition nets,Pr/T网）Pr/T网的转移发生条件和引起的标识变化是通过刻画标记性质的谓词
46、来解释的示例：一个机械制造车间零件加工的简化Pr/T网系统模型,-108-,一个机械制造车间零件加工的简化Pr/T网系统模型（1）,1,问题描述有一名工人分别在机床甲和机床乙上加工零件。先加工完的机床要等待另一台机床加工完后，零件经装配才能卸下。然后，机床转入空闲，再进入就绪。以上加工过程重复进行为简化问题，这里只考虑工人和机床的关系。其他如原材料来源、成品的去处，以及辅助工具（刀、量等）等一概不考虑,-109-,一个机械制造车间零件加工的简化Pr/T网系统模型（2）,2,P/T网系统模型,-110-,一个机械制造车间零件加工的简化Pr/T网系统模型（3）,3,先分析位置从上可知：本系统中有3
47、 个个体：工人、机床甲作和机床乙，用w、a、b来表示这3 个个体可能处于4 种状态：就绪（ready）、工作（working）、等待（waiting）和休息（resting）工作必须是w和a或w和b的结合，为了强调结合用joint（结合）表示working如果用P-元素表示4个状态，用w、a、b三个个体名代替没有个性的标记。就可把逻辑功能相同的位置（状态）折叠在一起这样位置由10个减少为4个,-111-,一个机械制造车间零件加工的简化Pr/T网系统模型（4）,逻辑功能相同的位置折叠在一起的图形表示,-112-,一个机械制造车间零件加工的简化Pr/T网系统模型（5）,在位置折叠的图中可见它保留了
48、P/T网系统中的全部有向孤和所有转移。有向张上旅弧上标注了孤上流动的个体或由个体结合而成的偶如w,a或w,bP-元素（位置）已不是原P/T网系统中的位置，而是其中个体当前的状态，即谓词。谓词中的标识也不是非负整数，而是由个体组成的集合。如P1中初始标识有3个个体，表明w、a、b都处于就绪状态。P2、P3和P4在初始标识下，均无个体，为空集。由此可见，引进谓词后，减少了P（位置）的个数,-113-,一个机械制造车间零件加工的简化Pr/T网系统模型（4）,4,再分析转移很明显，由上图可见：转移也可分为4类：结合（joint）（开始工作）=t1,t2、完成（finish）（工作完成）=t3,t4、装
49、配（assemble）=t5和准备（to-ready）=t6,t7,t8由上图还可见：同类转移有相同的前集和后集，t1与t2、t3与t4，以及t6、t7和t8之间的区别在于参与转移的个体不同。如果我们用变量x来代替个体名，则可把同类转移也合并为一个。这就可以得到合并转移后的网系统,-114-,一个机械制造车间零件加工的简化Pr/T网系统模型（5）,合并转移后得到的网系统,-115-,一个机械制造车间零件加工的简化Pr/T网系统模型（6）,在转移折叠的图中可见把P、T 两个元素间的多条有向弧合并为一条，弧上标注也用“+”号连在一起。如P1与t1、t2之间的两条弧合并为一条后，弧上记为w+x，x表
50、示P1中的任何一个个体。为统一符号，w,a和w,b可改写为w,x。用尖括号及“+”号连在一起的表达式为符号和必须指出，w+x是两个独立的个体，w,x是两个结合在一起的个体新转移joint、finish、assemble和to-ready分别代表系统中的同一类转移当从P1到joint的弧上标注w+x中的变量x取个体a为值时，转移joint发生就是原系统中t1的发生。当x以b为值时，joint发生不是t1，而是t2。但x不能以w为值图中只使用了一个变量名x，但x并非表示同一个变量。事实上，只有同一个转移的所有I/O弧上的变量才是同一个变量，它必须取同一个个体为值。由此可见，引进变量后减少了T-元素
