形式化开发方法(1)-Petri网

《形式化开发方法(1)-Petri网》由会员分享，可在线阅读，更多相关《形式化开发方法(1)-Petri网（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 双重类 兼有操作类和描述类两者

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网的基本原理-静态结构 P

7、etri网的基本原理-动态特征 建模实例 特性分析 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;F1）和N2=（P

11、2,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）上,-28-,转移发生规则（1）,

13、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） W（t,p） 当p * t t *

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

15、为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系统 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 容量有限，且不进行技术处理，则有可能发生碰撞,