搜索
第5章形式化开发方法•形式化方法：是建立在严格数学基础上，具有精确数学表达形式和语义的开发方法。其中：形式化方法的基本含义是借助数学的方法来研究软件工程中的有关问题。•特点：1.可以用数学方法进行验证。如代数方法；2.可以用算法进行识别和变换。例如：形式语言（BNF）、有限自动机（FA）等是形式化方法描述算法的程序流程图、类pascal、类C等算法描述语言则是非形式化方法。•形式化方法分类1.根据说明目标软件系统的方式，可以分为两类：1)面向模型的形式化方法通过构造一个数学模型来说明系统的行为。2)面向属性的形式化方法通过描述目标软件系统的各种属性来间接定义系统行为。2.根据表达能力，可以分为五类：1)基于模型的方法给出系统状态和状态变换操作的显式但亦是抽象的定义，即通过定义系统状态和操作建立系统模型。但对于并发没有显式的表示。如：Z语言，VDM，B方法等。2)基于逻辑的方法用逻辑描述系统预期的性能，包括底层规约、时序和可能性行为。采用与所选逻辑相关的公理系统证明系统具有预期的性能。用具体的编程构造扩充逻辑从而得到一种广谱形式化方法，通过保持正确性的细化步骤集来开发系统。如：ITL(区间时序逻辑),TAM(时序代理模型)，RTTL(实时时序逻辑)等3)代数方法通过联系不同操作间的行为关系而给出操作的显式定义，而不定义状态，同样它亦未给出并发的显式表示.如：OBJ，Clear，Larch族代数规约语言等4)进程代数方法给出并发过程的一个显式模型，并通过进程间允许的可观察的通讯上的限制（约束）来表示行为.如：CSP（通信顺序过程）ACP（通信过程代数）CCS（通信并发系统/通信系统演算）等5)基于网络的方法该方法采用具有形式语义的图形语言，根据网络中的数据流显式地给出系统的行为模型，包括数据在网中从一个结点流向另一个结点的条件、并发行等。如：Petri网、谓词变换网Petri网的提出：1962年由德国人C.A.Petri在他的博士论文：“用自动机通讯”(Communicationwithautomata)中首次提出的“网状结构的信息模型”其中“有限自动机—Finiteautomata”定义为：FA—A=（S，Σ，δ，S0，F）其中：S---状态集Σ---字母表δ---S×Σ→S的映射S0---开始状态/状态集F---终止状态集FA—A可用三种方式描述：集合法：定义方法；矩阵法：状态转换矩阵/表状态图法：状态转换图§5.1Petri网概述例子：一个保险箱上装了一把复合锁，锁有三个位置，分别标记为1、2、3，转盘可向左（L）或向右（R）转动。这样，在任意时刻转盘都有6种可能的运动如下：L1、R1、L2、R2、L3、R3保险箱的组合密码是：L1、R3、L2转盘的任何其他运动都将引起报警。123则保险箱拨动密码的状态转换情况如DFA的状态转换图所示：BASTEL1R3L2εεε其中：初态S：保险箱锁定终态T：保险箱解锁终态E：报警符号ε：转盘的任何其他移动转盘动作当前状态L1R1L2R2L3R3=SAEEEEEAEEEEEBBEETEEE保险箱DFA的状态转换表：其优点：1.简洁、直观2.严谨、无二义性3.可以从代数角度进行进一步的分析如上述DFA可以转换成如下代数方程组进一步进行分析讨论x=L1yy=R3zz=L3解该线性方程组得：L1R3L3说明：1.Petri网是利用FA的状态图发展起来的网系统2．Petri网是一种系统的数学和图形的描述和分析工具（密码）Petri网的特点：1.作为一种图形工具，直观形象，便于使用注：同软件设计中的状态图、结构图、程序流程图类似，直观形象，便于使用；如：用Petri网可直观描述具有并发、并行、异步、分布、不确定性和随机的信息处理系统，即模拟系统的动态性和并发性。2.作为一种数学工具，便于计算和验证如：它可以建立状态方程、代数方程以及系统行为的其他数学模型，便于计算和验证；3.作为一种理论与实际工作的中介（桥梁），相互借鉴如：实际工作者可以从中学到如何使他们的建模条理化理论工作者可以从中学到如何使他们的建模更实用化§5.2Petri网的定义及基本原理一、Petri网的静态结构（或称具有静态特征的Petri网）Petri网N=（P，T；F），并满足以下条件：(1)P∪T≠Φ(2)P∩T＝Φ(3)F⊆（P×T）∪（T×P）//双向映射关系(4)DOM(F)∪COD(F)=P∪T//表明P∪T中的元素//在N中均被使用到其中: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，p6}T={t1，t2，t3，t4，t5，t6}F={(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,t6}COD(F)=)={p1,t1,p2,t3,p3,p4,t4,t5,p5,p6}显然DOM(F)∪COD(F)=P∪T={p1,p2,p3,p4p5,p6,t1,t2,t3,,t4,t5,t6}注：此为关系集合表示法Petri网的图形表示：1．用圆形表示位置(库所)p:作用是决定转移能否发生2．用矩形表示转移(变迁)t:作用是改变位置的状态3．用有向弧→表示位置与转移的有序偶例如上述Petri网N的图形表示:•位置或转移的前集和后集定义：设X∈P∪T,令*x={y|(y,x)∈F}//前集（亦称x的输入集）x*={y|(x,y)∈F}//后集（亦称x的输出集）说明：定义两个特殊的Petri网1.纯网：如果对所有x∈P∪T，都有*x∩x*＝Φ注：表明x无自循环（仅通过一个结点的循环）2.简单网：如果对所有x，y∈P∪T,，都有(*x=*y)∧(x*=y*)＝(x=y)即：不存在两个不同的结点，它们的前集和后集相同。例如：上例是纯网且是简单网•非纯网例：P1t1P2其中：*t1={p1}t1*={p1，p2}*t1∩t1*={p1}∩{p1，p2}={p1}≠ΦP1t1P2或：其中：*p2={t1}p2*={t1}*p2∩p2*={t1}∩{t1}={t1}≠Φ其中：*t1={p1}，*t2={p1}，t1*={p2}，t2*={p2}然而t1≠t2P1t1P2t2•非简单网例：P1t1P2t2或：二、Petri网的动态特征具有动态特征的Petri网是一个六元组：∑=（P，T；F，K，W，M0）其中：（P，T；F）同前K:P→N+∪{ω}，是位置上的容量函数，表示一个位置的总容量N+={1，2，3，…}ω=∞：即，若K(P)=ω，表示位置的容量为无穷W:F→N+，是弧集合上的权函数M:P→N0，是∑的标识（Marking），M0为初始标识N0={0，1，2，3，…}∀p∈P⇒M(p)≤K(p)其中：M(p):表示当前位置p的实际存储数量。说明：在Petri网的图形表示中1．W（x,y）=i标在弧（x,y）上，即：xyixyi或其中：i=1可省略•••P1P2如：2．M(p)=i用在位置p对应的圆形中标注i个实心点标记其中：1)实心点“•”称作标记（Token）2)同一位置中的诸多标记代表同一类完全等价的个体如：其中一个标记代表人，则其他标记也代表人3．K(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)=1∀p:K(P)=ω3．转移发生规则Petri网的动态行为:是通过转移t发生引起标识M改变来体现的，下面是转移可发生的条件:（1）转移t可发生的条件若在标识M下，∀p1，p1∈*t=M(p1)≥W(p1，t)，且∀p2，p2∈t*=M(p2)+W(t，p2)≤K(p2)，此时称t在M下可发生，记为M[t＞例如:可发生例：●p1tp2K=1其中：M(p1)=1M(p2)=0W(p1，t)=1W(t，p2)=1K(p2)=1则有：M(p1)=1≥W(p1，t)=1且M(p2)+W(t，p2)=0+1=1≤K(p2)=1●p1tp2K=1不可发生例：条件1不成立：条件2不成立：●●p1tp2K=12(2)转移t发生的结果若M[t＞，t就可以发生，发生后将M变成新标识M′，记为M[t＞M′，(或M—M′)，并称M′为M的后继标识。对∀p∈P均进行如下操作：tM(p)-W(p，t)当p∈*t-t*(即：p∈*t且p∉t*)计算t的前驱位置标记数M(p)+W(t，p)当p∈t*-*t(即：p∉*t且p∈t*)计算t的后继位置标记数M(p)-W(p,t)+W(t,p)当p∈t*∩*t(即:p∈*t且p∈t*)同时计算t的前驱和后继位置标记数M(p)当p∉t*∪*t与t的发生无关的位置标记数M/(p)=例：（关于转移t发生的结果）p1●t1p2t2p3则：M=M0=(1，0，0)M[t1＞M′M′(p1)=M(p1)-W(p1，t1)=1-1M′=(0，1，0)M′(p2)=M(p2)+W(t1，p2)=0+1M′(p3)=M(p3)=0结果为：p1t1●p2t2p3a.p1●t1p2t2p3结果为：p1●t1●p2t2p3则：M=M0=(1，0，0)M[t1＞M′M′(p1)=M(p1)-W(p1,t1)+W(t1,p1)p1∈t1*∩*t1M′=(1,1,0)M′(p2)=M(p2)+W(t1，p2)p2∈t1*M′(p3)=M(p3)b.p1●t1●p2t2p3冲突：一个资源m(p2)=1t1、t2不能同时发生则：M=M0=(1，1，0)M[t1＞M′M′(p1)=M(p1)-W(p1，t1)p1∈*t1M′=(0,1,0)M′(p2)=M(p2)-W(p2,t1)+W(t1,p2)p2∈t1*∩*t1M′(p3)=M(p3)p1t1●p2t2p3结果为：c.说明：1.一个没有任何输入位置的转移叫做源转移，一个源转移的发生是无条件的且它的发生只会产生标记，而不消耗任何标记。tp●tp2．一个没有任何输出位置的转移叫做潭转移，一个潭转移的发生将消耗标记，而不产生任何标记。利用下例Petri网进一步讨论在该Petri网中，初始标记为：M0=(1，0，0，0，0，0)1．由转移t发生条件，这时有M0[t1＞和M0[t3＞2．转移t发生的结果和现象•冲突(Conflict)：由于M0[t1＞且M0[t3＞，表明t1和t3都可以发生，而M0(p1)=1，即t1和t3共享一个“资源”，则t1和t3不能同时发生，网论中称这种情况为“冲突”。•网论解决冲突的办法可以是：通过环境对系统进行控制其中：环境：指具体情况。控制：指给出一定的条件和限制。如：启动次数（权1）+优先级（权2）令：t1的优先级＞t3的优先级且t1发生次数≤t3发生次数，则此时：M0[t1＞但ᄀM0[t3＞t1发生有：M0[t1＞M1=(0，1，0，0，0，0)M1[t2＞M0=(1，0，0，0，0，0)此时M0[t1＞且M0[t3＞但t1发生次数＞t3发生次数，则M0[t3＞但ᄀM0[t1＞t3发生有：M0[t3＞M2=(0，0，1，1，0，0)这时出现（产生）并发：•并发(Concur