《高级软件工程第5章形式化开发方法1》由会员分享，可在线阅读，更多相关《高级软件工程第5章形式化开发方法1（35页珍藏版）》请在金锄头文库上搜索。
1、第第5章章形式化开发方法形式化开发方法形式化方法：是建立在形式化方法：是建立在严严格数学基格数学基础础上，具有精确数学上，具有精确数学表达表达形式形式和和语义语义的开的开发发方法。方法。其中：形式化方法的基本含其中：形式化方法的基本含义义是借助数学的方法来研究是借助数学的方法来研究软软件工程中的有关件工程中的有关问题问题。特点：特点：1.可以用数学方法进行验证。如代数方法；可以用数学方法进行验证。如代数方法；2.可以用算法进行识别和变换。可以用算法进行识别和变换。例如：例如：形式语言（形式语言（BNF）、有限自动机（）、有限自动机（FA）等是形式化方法）等是形式化方法描述算法的程序流程图、类描
2、述算法的程序流程图、类pascal、类、类C等算法描述语言等算法描述语言则是非形式化方法。则是非形式化方法。形式化方法分类形式化方法分类1.根据说明目标软件系统的方式，可以分为两类：根据说明目标软件系统的方式，可以分为两类：1)面向模型的形式化方法面向模型的形式化方法通过构造一个数学模型来说明系统的行为。通过构造一个数学模型来说明系统的行为。2)面向属性的形式化方法面向属性的形式化方法通过描述目标软件系统的各种属性来间接定义系统行为。通过描述目标软件系统的各种属性来间接定义系统行为。2.根据表达能力，可以分为五类：根据表达能力，可以分为五类：1)基于模型的方法基于模型的方法给出系统状态和状态变
3、换操作的显式但亦是抽象的定义，即通给出系统状态和状态变换操作的显式但亦是抽象的定义，即通过定义系统状态和操作建立系统模型。但对于并发没有显式的表过定义系统状态和操作建立系统模型。但对于并发没有显式的表示。示。如：如：Z语言，语言，VDM，B方法等。方法等。2)基于逻辑的方法基于逻辑的方法用逻辑描述系统预期的性能，包括底层规约、时序和可能性行用逻辑描述系统预期的性能，包括底层规约、时序和可能性行为。采用与所选逻辑相关的公理系统证明系统具有预期的性能。为。采用与所选逻辑相关的公理系统证明系统具有预期的性能。用具体的编程构造扩充逻辑从而得到一种广谱形式化方法，通过用具体的编程构造扩充逻辑从而得到一种
4、广谱形式化方法，通过保持正确性的细化步骤集来开发系统。保持正确性的细化步骤集来开发系统。如：如：ITL(区间时序逻辑区间时序逻辑),TAM(时序代理模型时序代理模型)，RTTL(实时时序逻辑实时时序逻辑)等等3)代数方法代数方法通过联系不同操作间的行为关系而给出操作的显式定通过联系不同操作间的行为关系而给出操作的显式定义，而不定义状态，同样它亦未给出并发的显式表示义，而不定义状态，同样它亦未给出并发的显式表示.如：如：OBJ，Clear，Larch族代数规约语言等族代数规约语言等4)进程代数方法进程代数方法给出并发过程的一个显式模型，并通过进程间允许的给出并发过程的一个显式模型，并通过进程间允
5、许的可观察的通讯上的限制（约束）来表示行为可观察的通讯上的限制（约束）来表示行为.如：如：CSP（通信顺序过程）（通信顺序过程）ACP（通信过程代数）（通信过程代数）CCS（通信并发系统（通信并发系统/通信系统演算通信系统演算）等）等5)基于网络的方法基于网络的方法该方法采用具有形式语义的图形语言，根据网络中的该方法采用具有形式语义的图形语言，根据网络中的数据流显式地给出系统的行为模型，包括数据在网中从数据流显式地给出系统的行为模型，包括数据在网中从一个结点流向另一个结点的条件、并发行等。一个结点流向另一个结点的条件、并发行等。如：如：Petri网、谓词变换网网、谓词变换网PetriPetri
6、网的提出：网的提出： 19621962年年由由德德国国人人C.A.PetriC.A.Petri在在他他的的博博士士 论论文：文：“用自用自动动机通机通讯讯” (Communication with automata)(Communication with automata)中首次提出的中首次提出的“网状网状结结构的信息模型构的信息模型” 其中其中“有限自有限自动动机机Finite automataFinite automata”定定义为义为： FAFAA=A=（S S，S S0 0，F F）其中：其中：S-S-状态集状态集 -字母表字母表 -S-SSS的映射的映射 S S0 0-开始状态开始状
7、态/ /状态集状态集 F-F-终止状态集终止状态集 FAFAA A可用三种方式描述：可用三种方式描述：集合法：定义方法；集合法：定义方法；矩阵法：状态转换矩阵矩阵法：状态转换矩阵/表表状态图法：状态转换图状态图法：状态转换图5.1Petri网概述网概述 例子：例子：一个保险箱上装了一把复合锁，锁有三个位置，分别一个保险箱上装了一把复合锁，锁有三个位置，分别标记为标记为1、2、3，转盘可向左（，转盘可向左（L）或向右（）或向右（R）转动。）转动。这样，在任意时刻转盘都有这样，在任意时刻转盘都有6种可能的运动如下：种可能的运动如下：L1、R1、L2、R2、L3、R3保险箱的组合密码是：保险箱的组合
8、密码是：L1、R3、L2转盘的任何其他运动都将引起报警。转盘的任何其他运动都将引起报警。123则保则保险箱拨动密码的状态转换情况如险箱拨动密码的状态转换情况如DFA的状态转换图的状态转换图所示：所示：BASTEL1R3L2其中：初态其中：初态S：保险箱锁定：保险箱锁定终态终态T：保险箱解锁：保险箱解锁终态终态E：报警：报警符号符号：转盘的任何其他移动：转盘的任何其他移动转盘动作转盘动作当前状态当前状态L1R1L2R2L3R3=SAEEEEEAEEEEEBBEETEEE保保险箱险箱DFA的状态转换表：的状态转换表：其优点：其优点：1.简洁、直观简洁、直观2.严谨、无二义性严谨、无二义性3.可以从
9、代数角度进行进一步的分析可以从代数角度进行进一步的分析如如上上述述DFA可可以以转转换换成成如如下下代代数数方方程程组组进进一一步步进进行行分分析析讨论讨论x =L1yy =R3z z =L3解该线性方程组得：解该线性方程组得：L1R3L3说明：说明：1.Petri网是利用网是利用FA的状态图发展起来的网系统的状态图发展起来的网系统2Petri网是一种系统的数学和图形的描述和分析工具网是一种系统的数学和图形的描述和分析工具（密码）（密码）Petri网的特点：网的特点：1.作为一种图形工具，直观形象，便于使用作为一种图形工具，直观形象，便于使用注：同软件设计中的状态图、结构图、程序流程图类注：同
10、软件设计中的状态图、结构图、程序流程图类似，直观形象，便于使用；似，直观形象，便于使用；如：用如：用Petri网可直观描述具有并发、并行、异步、分网可直观描述具有并发、并行、异步、分布、不确定性和随机的信息处理系统，即模拟系布、不确定性和随机的信息处理系统，即模拟系统的动态性和并发性。统的动态性和并发性。2.作为一种数学工具，便于计算和验证作为一种数学工具，便于计算和验证如：它可以建立状态方程、代数方程以及系统行为的如：它可以建立状态方程、代数方程以及系统行为的其他数学模型，便于计算和验证；其他数学模型，便于计算和验证；3.作为一种理论与实际工作的中介（桥梁），相互借鉴作为一种理论与实际工作的
11、中介（桥梁），相互借鉴如：如：实际工作者可以从中学到如何使他们的建模条理化实际工作者可以从中学到如何使他们的建模条理化理论工作者可以从中学到如何使他们的建模更实用化理论工作者可以从中学到如何使他们的建模更实用化5.2Petri网的定义及基本原理网的定义及基本原理一、一、Petri网的静态结构（或称具有静态特征的网的静态结构（或称具有静态特征的Petri网）网）Petri网网N=（P，T；F），并满足以下条件：），并满足以下条件：(1)PT(2)PT(3)F（PT）（TP）/双向映射关系双向映射关系(4)DOM(F)COD(F)=PT/表明表明PT中的元素中的元素/在在N中均被使用到中均被使用到
12、其中其中:P=p1,p2,pn是是N的有穷位置集合的有穷位置集合(表示状态的元素表示状态的元素)T=t1,t2,tn是是N的有穷转移集合的有穷转移集合(表示状态变化的元素表示状态变化的元素)F是由一个是由一个P元素和一个元素和一个T元素组成的二元组的集合元素组成的二元组的集合DOM(F)=x|y:(y,x)F/代表代表F的后集的后集;存在量词存在量词COD(F)=x|y:(x,y)F/代表代表F的前集；的前集；注：位置注：位置(Place)有人译为有人译为“库所库所”，转移，转移(Transition)译成译成“变迁变迁”例例1：N=(P,T;F)P=p1，p2，p3，p4，p5，p6T=t1
13、，t2，t3，t4，t5，t6F=(p1,t1),(t1,p2),(p2,t2),(t1,p1),(p1,t3),(t3,p3),(t3,p4),(p3,t4),(p4,t5),(t4,p5),(t5,p6),(p5,t6),(p6,t6)其中：其中：DOM(F)=t1,p2,t2,p1,t3,p3,p4,t4,t5,p5,p6,t6COD(F)=)=p1,t1,p2,t3,p3,p4,t4,t5,p5,p6显然显然DOM(F)COD(F)=PT=p1,p2,p3,p4p5,p6,t1,t2,t3,t4,t5,t6注：此为关系集合表示法注：此为关系集合表示法Petri网的图形表示：网的图形表示
14、：1用圆形用圆形表示位置表示位置(库所库所)p:作用是决定转移能否发生作用是决定转移能否发生2用矩形用矩形表示转移表示转移(变迁变迁)t:作用是改变位置的状态作用是改变位置的状态3用有向弧用有向弧表示位置与转移的有序偶表示位置与转移的有序偶例如上述例如上述Petri网网N的图形表示的图形表示:位置或转移的前集和后集定义：位置或转移的前集和后集定义：设设XPT,令令*x=y|(y,x)F/前集（亦称前集（亦称x的输入集）的输入集）x*=y|(x,y)F/后集（亦称后集（亦称x的输出集）的输出集）说明：定义两个特殊的说明：定义两个特殊的Petri网网1.纯网：如果对所有纯网：如果对所有xPT，都有
15、，都有*xx*注：表明注：表明x无自循环（仅通过一个结点的循环）无自循环（仅通过一个结点的循环）2.简单网：如果对所有简单网：如果对所有x，yPT,，都有，都有(*x=*y)(x*=y*)(x=y)即：不存在两个不同的结点，它们的前集和后集相同。即：不存在两个不同的结点，它们的前集和后集相同。例如：上例是纯网且是简单网例如：上例是纯网且是简单网非纯网例：非纯网例：P1t1P2其中：其中： *t1=p1t1*=p1，p2*t1t1*=p1p1，p2=p1P1t1P2或：或：其中：其中： *p2=t1p2*=t1*p2p2*=t1t1=t1其中：其中：*t1=p1，*t2=p1，t1*=p2，t2
16、*=p2然而然而t1t2P1t1P2t2非简单网例：非简单网例：P1t1P2t2或：或：二、二、Petri网的动态特征网的动态特征具有动态特征的具有动态特征的Petri网是一个六元组：网是一个六元组：=（P，T；F，K，W，M0）其中：（其中：（P，T；F）同前）同前K:PN+，是位置上的容量函数，表示一个位置，是位置上的容量函数，表示一个位置的总容量的总容量N+=1，2，3，=：即，若：即，若K(P)=，表示位置的容量为无穷，表示位置的容量为无穷W:FN+，是弧集合上的权函数，是弧集合上的权函数M:PN0，是，是的标识（的标识（Marking），），M0为初始标识为初始标识N0=0，1，2，
17、3，pPM(p)K(p)其中：其中：M(p):表示当前位置表示当前位置p的实际存储数量。的实际存储数量。说明：在说明：在Petri网的图形表示中网的图形表示中1W（x,y）=i 标在弧（标在弧（x,y）上，即：）上，即：xyixyi或或其中：其中：i=1可省略可省略P1P2如：如：2M(p)=i 用在位置用在位置p对应的圆形中标注对应的圆形中标注i个实心点标记个实心点标记其中：其中：1)实心点实心点“”称作标记（称作标记（Token）2)同一位置中的诸多标记代表同一类完全等价的个体同一位置中的诸多标记代表同一类完全等价的个体如：其中一个标记代表人，则其他标记也代表人如：其中一个标记代表人，则其
18、他标记也代表人3K(p)标记在位置标记在位置p的圆形外面，如的圆形外面，如K(p)=10则有：则有：K=10其中：其中：K(p)=时省略不标时省略不标例：设有例：设有Petri网网 则有：则有：M0=(1，0，0，0，0，0)W(t2,p1)=W(t5,p6)=W(t6,p1)=2W(t3,p3)=4W(t4,p5)=3W(p1,t1)=W(t1,p2)=W(p2,t2)=W(p1,t3)=W(t3,p4)=W(p4,t5)=W(p3,t4)=W(p5,t6)=W(p6,t6)=1p:K(P)=3转移发生规则转移发生规则Petri网的动态行为网的动态行为:是通过转移是通过转移t发生引起标识发生
19、引起标识M改变来改变来体现的，下面是转移可发生的条件体现的，下面是转移可发生的条件:（1）转移）转移t可发生的条件可发生的条件若在标识若在标识M下，下，p1，p1*t=M(p1)W(p1，t)，且且p2，p2t*=M(p2)+W(t，p2)K(p2)，此时称此时称t在在M下可发生，记为下可发生，记为Mt 例如例如:可发生例：可发生例：p1tp2K=1其中：其中：M(p1)=1M(p2)=0W(p1，t)=1W(t，p2)=1K(p2)=1则有：则有：M(p1)=1W(p1，t)=1且且M(p2)+W(t，p2)=0+1=1K(p2)=1p1tp2K=1不可发生例：不可发生例：条件条件1不成立：
20、不成立：条件条件2不成立：不成立：p1tp2K=12(2)转移转移t发生的结果发生的结果若若Mt，t就可以发生，发生后将就可以发生，发生后将M变成新标识变成新标识M，记为记为MtM，(或或MM)，并称，并称M为为M的后继标的后继标识。对识。对pP均进行如下操作：均进行如下操作： tM(p)-W(p，t)当当p*t-t*(即：即：p*t且且p t*)计算计算t的前驱位置标记数的前驱位置标记数M(p)+W(t，p)当当pt*-*t(即：即：p *t且且pt*)计算计算t的后继位置标记数的后继位置标记数M(p)-W(p,t)+W(t,p)当当pt*t(即即:p*t且且pt*)同时计算同时计算t的前驱
21、和后继位置标记数的前驱和后继位置标记数M(p)当当p t*t与与t的发生无关的位置标记数的发生无关的位置标记数M/(p)=例：（关于转移例：（关于转移t发生的结果）发生的结果）p1t1p2t2p3则：则：M=M0=(1，0，0)Mt1MM(p1)=M(p1)-W(p1，t1)=1-1M=(0，1，0)M(p2)=M(p2)+W(t1，p2)=0+1M(p3)=M(p3)=0结果为：结果为：p1t1p2t2p3a.p1t1p2t2p3结果为：结果为：p1t1p2t2p3则：则：M=M0=(1，0，0)Mt1MM (p1)=M(p1)-W(p1,t1)+W(t1,p1)p1t1*t1M =(1,1
22、,0)M (p2)=M(p2)+W(t1，p2)p2t1*M (p3)=M(p3)b.p1t1p2t2p3冲突：一个资源冲突：一个资源m(p2)=1t1、t2不能同时发生不能同时发生则：则：M=M0=(1，1，0)Mt1MM (p1)=M(p1)-W(p1，t1)p1*t1M =(0,1,0)M (p2)=M(p2)-W(p2,t1)+W(t1,p2)p2t1*t1M (p3)=M(p3)p1t1p2t2p3结果为：结果为：c.说明：说明：1.一个没有任何输入位置的转移叫做源转移，一个源转移一个没有任何输入位置的转移叫做源转移，一个源转移的发生是无条件的且它的发生只会产生标记，而不消耗的发生是
23、无条件的且它的发生只会产生标记，而不消耗任何标记。任何标记。tptp2一个没有任何输出位置的转移叫做潭转移，一个潭转一个没有任何输出位置的转移叫做潭转移，一个潭转移的发生将消耗标记，而不产生任何标记。移的发生将消耗标记，而不产生任何标记。利用下例利用下例Petri网进一步讨论网进一步讨论在该在该Petri网中，初始标记为：网中，初始标记为：M0=(1，0，0，0，0，0)1由转移由转移t发生条件，这时有发生条件，这时有M0t1和和M0t32转移转移t发生的结果和现象发生的结果和现象冲突冲突( (Conflict) )： 由于由于M0t1且且M0t3，表明，表明t1和和t3同时可以发生，而同时可
24、以发生，而 M0(p1)=1，即，即t1和和t3共享一个共享一个“资源资源”，则，则t1和和t3不能同时不能同时发发 生，网论中称这种情况为生，网论中称这种情况为“冲突冲突”。网论解决冲突的办法可以是：通过环境对系统进行控制网论解决冲突的办法可以是：通过环境对系统进行控制其中：环境：指具体情况。其中：环境：指具体情况。控制：指给出一定的条件和限制。控制：指给出一定的条件和限制。如：启动次数（权如：启动次数（权1）+优先级（权优先级（权2）令：令：t1的优先级的优先级t3的优先级的优先级且且t1发生次数发生次数t3发生发生次数，则此时：次数，则此时：M0t1但但M0t3t1发生有：发生有：M0t
25、1M1=(0，1，0，0，0，0)M1t2M0=(1，0，0，0，0，0)此时此时M0t1且且M0t3但但t1发生次数发生次数t3发生次数，则发生次数，则M0t3但但M0t1t3发生有：发生有：M0t3M2=(0，0，1，1，0，0) 这时出现（产生）并发：这时出现（产生）并发：并发并发(Concurrent)M2(p3)=1和和M2(p4)=1两两件件事事同同时时出出现现，此此时时t4和和t5同同时时可以发生，且互不影响，网论中称这种现象为可以发生，且互不影响，网论中称这种现象为“并发并发”并行（并行（Parallel）t4和和t5同时发生。发生后，则得标记：同时发生。发生后，则得标记：M=
26、(0，0，0，0，1，1)此时此时Mt6，若，若t6发生，则有：发生，则有：Mt6M0=(1，0，0，0，0，0)，说明：说明：1.t6起着使起着使t4、t5两个异步（不在同一条执行路径上）两个异步（不在同一条执行路径上）活动同步（在同一条执行路径上）的作用。活动同步（在同一条执行路径上）的作用。2.并发：是两件以上的事情同时发生，是瞬时的事件并发：是两件以上的事情同时发生，是瞬时的事件3.并行：是两件以上的进程同时运行，是持续的过程并行：是两件以上的进程同时运行，是持续的过程4并发和并行的关系：并发可导致并行，但并行的事并发和并行的关系：并发可导致并行，但并行的事件件并并不不一一定定是是并并
27、发发的的。一一般般情情况况下下说说“并并发发”也也有有并行的含义并行的含义,但反之不一定成立。但反之不一定成立。碰撞碰撞(contact)设有设有M0=(1，0，1，0，0，0)，并规定位置容量均，并规定位置容量均为为K=1(不能超过不能超过1)，这时，这时t3不能发生，因为不能发生，因为t3的发生的发生会使会使p3的容量超过的容量超过1，称这种现象为，称这种现象为“碰撞碰撞”。混惑混惑(confusion)： 有时，一个有时，一个Petri网中同时存在着并发和冲突，而且并网中同时存在着并发和冲突，而且并发的实施会引起冲突的消失发的实施会引起冲突的消失(减少减少)或出现或出现(增加增加)，我们
28、，我们称这种情况为称这种情况为“混惑混惑”。例：在下图所示的例：在下图所示的PetriPetri网中网中 p2p1p3p4p5M0=(1,1,0,0,0)此时此时M0t1且且M0t3（并发），若（并发），若t3发生，则有发生，则有M=(1,0,1,0,0)p2p1p3p4p5使使Mt1且且Mt2，出现，出现“冲突冲突”，因共享，因共享p1中的一个中的一个“资源资源”，说明说明“并发并发”的存在，使原没有的存在，使原没有“冲突冲突”，出现了，出现了“冲突冲突”。说明：存在说明：存在“混惑混惑的系统不是好系统，因为在这种系统中，的系统不是好系统，因为在这种系统中， 冲突忽隐忽现，使得外部环境对系统
29、难以控制。冲突忽隐忽现，使得外部环境对系统难以控制。关于关于“并发并发和和“冲突冲突”两个概念的形式化（完整）两个概念的形式化（完整）描述描述1并发并发设设M为为Petri网网的一个标识，若存在的一个标识，若存在t1和和t2使得使得Mt1和和Mt2，并满足：，并满足：Mt1M1=M1t2且且Mt2M2=M2t1则称则称t1和和t2在在M下并发。下并发。即：在即：在M标识下，标识下，t1和和t2都可发生，且它们当中任一个转都可发生，且它们当中任一个转移发生都不会使另一个转移不发生。移发生都不会使另一个转移不发生。2冲突冲突设设M为为Petri网网的一个标识，若存在的一个标识，若存在t1和和t2使
30、得使得Mt1和和Mt2，并满足：，并满足：Mt1M1=M1t2且且Mt2M2=M2t1则称则称t1和和t2在在M下冲突。下冲突。 即：即：M标识下，标识下，t1和和t2都可发生，但都可发生，但t1和和t2中只有一个能中只有一个能 发生，而且其中任一个转移发生都会使另一个转移发生，而且其中任一个转移发生都会使另一个转移 不发生。不发生。 简单简单Petri网：（习惯上把）满足下述条件的网：（习惯上把）满足下述条件的Petri网网(1)pP：K(p)=(2)(x，y)F：W(x，y)=1对于简单对于简单Petri网，可以简记为：网，可以简记为：=（N，M）=（P，T；M）对于简单对于简单Petri
31、网，其运行发生规则可以简化为：网，其运行发生规则可以简化为：发生条件：若发生条件：若MtpP:M(p)1发生结果：发生结果：M(p)-1当当p*t-t*M(p)=M(p)+1当当pt*-*tM(p)其它（包括其它（包括pt*t）说明：简单说明：简单Petri网即为传统的网即为传统的Petri网。而把有限容量和网。而把有限容量和权值为任意大于等于权值为任意大于等于1的整数的的整数的Petri网称为网称为P/T网网P/T网：满足下述条件的网：满足下述条件的Petri网网(1)pP：K(p)=i (i=n) i (i=1)说明：可以证明，每个说明：可以证明，每个P/T网都可以改造成为其行网都可以改造成为其行为等效的（并行化）简单为等效的（并行化）简单Petri网。所以，网。所以，下面讨论的简单下面讨论的简单Petri网的基本性质，也都网的基本性质，也都适用于适用于P/T网。网。
